On this page:
1 Introduction
2 Meetings
3 Structure
4 Readings, Assignments, Grades, Turn Ins

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 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)




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 Foundationsand 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.