Software Foundations (Winter 2013)

This class is taught by Jay McCarthy. Call him Jay.

We meet in 1018 JKB at 9-9:40a MWF.

Jay McCarthy’s office hours are 6am to noon MWRF, excluding class time, in 3328 TMCB.

There is a mailing list hosted at Google Groups. Use it to ask non-revealing questions and receive answers, as well as general course announcements. You are responsible for reading the content of this mailing list.

1 Introduction

This is a course on the mathematical theory of programming, from a technical and formal perspective. We use the excellent open source textbook Software Foundations, by Benjamin Pierce.

2 Meetings

	Week		Chapter
	Week 0 (01/07, 01/09, 01/11)		Preface & Basics: Functional Programming and Reasoning About Programs
	Week 1 (01/14, 01/16, 01/18)		Lists: Working with Structured Data
	Week 2 (01/23, 01/25)		Poly: Polymorphism and Higher-Order Functions
	Week 3 (01/28, 01/30, 02/01)		Gen: Generalizing Induction Hypotheses
	Week 4 (02/04, 02/06, 02/08)		Prop: Propositions and Evidence
	Week 5 (02/11, 02/13, 02/15)		Logic: Logic in Coq
	Week 6 (02/19, 02/20, 02/22)		Imp: Simple Imperative Programs
	Week 7 (02/25, 02/27, 03/01)		ImpCEvalFun: An Evaluation Function for Imp & Extraction: Extracting ML from Coq
	Week 8 (03/05, 03/06, 03/08)		Equiv: Program Equivalence
	Week 9 (03/11, 03/13, 03/15)		Hoare: Hoare Logic
	Week 10 (03/18, 03/20, 03/22)		Rel: Properties of Relations & HoareAsLogic: Hoare Logic as a Logic
	Week 11 (03/25, 03/27, 03/29)		Smallstep: Small-Step Operational Semantics
	Week 12 (04/01, 04/03, 04/05)		Review
	Week 13 (04/08, 04/10, 04/12)		Types: Type Systems
	Week 14 (04/15)		Stlc: The Simply Typed Lambda Calculus

This schedule may change.

3 Structure

The course is structured as follows: each week, I will lecture on Monday, from a chapter in the textbook. By Wednesday, you should try out some of the exercises for the week and be prepared to talk about some of them in class, which we will do during the class period. On Friday, after you’ve turned in the assignment for the week, we’ll review the exercises in more detail and finish any loose ends for the chapter.

By 5PM on the Wednesday of each week, send me a checkpoint of your work where the turnin number is ${Week}.0. For example, on Wednesday the 9th of January, you would send turnin 0.0.

By 9AM on the Monday of the next week, send me a checkpoint of your work where the turnin number is ${Week}.5. For example, on Monday the 14th of January, you would send turnin 0.5.

In Week 2, we don’t meet on Monday, so you should turn in 1.5 on Wednesday (the 23rd), 2.0 on Friday (the 25th), and 2.5 on Monday (the 28th).

On Weeks 7 and 10, we do two chapters. You’ll find that one chapter is easy, so you are likely to just get bonus points for finishing it faster. But we won’t change the due dates in any way.

In Week 14, we don’t meet on Wednesday or Friday, so only send in a single turnin by the day of the final (April 20th) named 14.0. (Essentially, the final chapter’s exercises are your final.)

This means that if you do all the turnins, you won’t have 14.5.

4 Readings, Assignments, Grades, Turn Ins

This course revolves around its textbook—Software Foundations—and the Coq Proof Assistant. You need to install both. The text below explains how to setup the textbook install. You’ll need to go to the Coq site yourself to install it. (But, of course, I’m happy to help you get it installed.)

The first thing you need to do in this course is to download the grading system:

You’ll need to have git installed, obvs.

git clone git://github.com/jeapostrophe/sf-check.git

cd sf-check

Then, create a directory for your homework based on your NetID:

mkdir -p students/${NETID}

cd students/${NETID}

Then, download and extract the textbook:

curl http://www.cis.upenn.edu/~bcpierce/sf/sf.tar.gz | tar xzvf -

As you do work in the class, you’ll be editing files in the sf directory.

You could also make a link from the sf directory to the next turnin directory and copy it each time.

When you are ready to make a turnin, then run:

cp -fr sf ${N}

when ${N} is a turnin’s number.

After you do that, you can check what grade you’ll get on the assignment by running:

You’ll need Racket installed, obvs.

racket coq.rkt

from the sf-check directory.

If you are satisfied with your grade, run:

tar cvzf ${NETID}-${N}.tgz students/${NETID}/${N}

and email ${NETID}-${N}.tgz to jay@cs.byu.edu with the subject line "BYU - Winter 2013 - CS 430 - $N". I’ll untar it on my end and run the same grading script to figure out your grade.

The sf-check README.md file describes the grading system. If I need to change anything, I’ll announce that you should run:

git pull

in the sf-check directory to get the changes.

1	Introduction
2	Meetings
3	Structure
4	Readings, Assignments, Grades, Turn Ins