Preface
(* Version of 4/21/2010 *)
These are notes for a one-semester course on Software
Foundations -- the mathematical theory of programming and
programming languages -- suitable for graduate or upper-level
undergraduate students. They develop basic concepts of functional
programming, logic, operational semantics, lambda-calculus, and
static type systems, using the Coq proof assistant.
The main novelty of the course is that the development is
formalized and machine-checked: the text is literally a script for
the Coq proof assistant. It is intended to be read hand-in-hand
with the accompanying Coq source file in an interactive session
with Coq. All the details of the lectures are fully developed in
Coq, and the exercises are designed to be worked using Coq.
The files are organized into a sequence of "core chapters,"
covering about one semester's worth of material and organized into
a coherent linear narrative, plus some "appendices" covering
additional topics.
The notes come in two variants: a "terse version" for use in
lectures and a "full version" that can be read outside of class
and used as a template for homework assignments.
Some fundamental themes of the course:
These notes are intended to be accessible to a broad range of
readers, from advanced undergraduates to PhD students. They
assume little specific background in programming languages or
logic. However, a degree of mathematical maturity will be
helpful.
Our laboratory for this course is the Coq proof assistant.
Coq can be seen as a combination of two things:
Coq runs on Windows and pretty much all flavors of Unix (including
Linux and OS X). You will need:
A tar file containing the full sources for the "release version"
of these notes (as a collection of Coq scripts and HTML files) is
available here:
Each chapter of the notes includes numerous exercises. Some are
marked "optional"; those that are not should be considered as
recommended. Doing just the recommended exercises should provide
good coverage of the material in approximately six or eight hours
of study time.
The "star ratings" for the exercises can be interpreted as follows:
Students who want additional texts to supplement and deepen what
they find here can have a look at these (among many others):
If you are an instructor and intend to use these materials in your
own course, you will undoubtedly find things you'd like to change,
improve, or add. Your contributions are welcome!
Please send an email to Benjamin Pierce, and we can set you up
with read/write access to our subversion repository and
developers' mailing list; in the repository you'll find a README
with further instructions.
Overview
- Logic: The mathematical basis for software engineering...
logic calculus -------------------- = ---------------------------- software engineering mechanical/civil engineering
- In particular, inductively defined sets and relations and
inductive proofs about them are ubiquitous in all of computer
science.
- In particular, inductively defined sets and relations and
inductive proofs about them are ubiquitous in all of computer
science.
- Functional programming: An increasingly important part of
the software developer's bag of tricks
- Advanced programming idioms in mainstream software
development methodologies are increasingly incorporating
ideas from functional programming.
- In particular, using persistent data structures and avoiding
mutable state enormously simplifies many concurrent
programming tasks.
- Advanced programming idioms in mainstream software
development methodologies are increasingly incorporating
ideas from functional programming.
- Foundations of programming languages (the second part of the
course):
- Notations and techniques for rigorously describing and
stress-testing new programming languages and language
features. (This is a surprisingly common activity! Most
large software systems include subsystems that are basically
programming languages -- think of regular expressions,
command-line formats, preference and configuration files,
SQL, Flash, PDF, etc., etc.)
- A more sophisticated understanding of the everyday tools
used to build software... what's going on under the hood of
<your favorite programming language>.
- Notations and techniques for rigorously describing and
stress-testing new programming languages and language
features. (This is a surprisingly common activity! Most
large software systems include subsystems that are basically
programming languages -- think of regular expressions,
command-line formats, preference and configuration files,
SQL, Flash, PDF, etc., etc.)
- Coq: An industrial-strength proof assistant
- Proof assistants are becoming more and more popular in both software and (especially) hardware industries. Coq is not the only one in widespread use, but learning one thoroughly will give you a big advantage in coming to grips with another.
Practicalities
Required Background
Coq
- a simple and slightly idiosyncratic (but, in its way, extremely expressive) programming language, together with
- a set of tools for stating logical assertions (including assertions about the behavior of programs) and marshalling evidence of their truth.
System Requirements
- A current (8.2) installation of Coq (available from the Coq home page).
- An IDE for interacting with Coq. Currently, there are two choices:
- Proof General is an Emacs-based IDE. It tends to be preferred by users who are already comfortable with Emacs. It requires a separate installation (google "Proof General").
- CoqIDE is a simpler stand-alone IDE. It is distributed with Coq, but on some platforms compiling it involves installing additional packages for GUI libraries and such.
Access to the Coq files
http://www.cis.upenn.edu/~bcpierce/sf
If you are using the notes as part of a class, you may be given
access to a locally extended version of the files, which you
should then use instead of the release version.
Exercises
- One star: easy exercises that most readers should take only a
minute or two. None of these are explicitly marked
"Recommended"; rather, all of them should be considered as
recommended: readers should be in the habit of working them
as they reach them.
- Two stars: straightforward exercises (five or ten minutes).
- Three stars: exercises requiring a bit of thought (fifteen
minutes to half an hour).
- Four stars: more difficult exercises (an hour or two).
Recommended reading
- Types and Programming Languages, by Benjamin C. Pierce. MIT
Press, 2002.
- Interactive Theorem Proving and Program Development: Coq'Art:
The Calculus of Inductive Constructions, by Yves Bertot and
Pierre Castéran. Springer-Verlag, 2004.
- Certified Programming with Dependent Types, by Adam Chlipala.
A draft textbook on practical proof engineering with Coq,
available from his web page.
- Practical Foundations for Programming Languages, by Robert
Harper. Manuscript, available from his web page.
- The Formal Semantics of Programming Languages: An
Introduction, by Glynn Winskel. MIT Press, 1993.
- Foundations for Programming Languages, by John C. Mitchell. MIT Press, 1996.