Preface
(* Preface
Version of 9/10/2009 *)
Version of 9/10/2009 *)
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 novel feature of the course is that the development is formalized and machine-checked: the text is literally a script for the Coq proof assistant. The notes are intended to be read hand-in-hand with the accompanying Coq source file in an interactive session with Coq under either CoqIDE or Proof General. All the details of the lectures are fully developed in Coq, and all the exercises are designed to be worked in an interactive Coq session.
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 a number of "appendices" covering additional topics.
The notes come in two variants: a "terse version" for lectures and a "full version" with much more text that can be read carefully outside of class and used as a template for homework assignments.
The main novel feature of the course is that the development is formalized and machine-checked: the text is literally a script for the Coq proof assistant. The notes are intended to be read hand-in-hand with the accompanying Coq source file in an interactive session with Coq under either CoqIDE or Proof General. All the details of the lectures are fully developed in Coq, and all the exercises are designed to be worked in an interactive Coq session.
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 a number of "appendices" covering additional topics.
The notes come in two variants: a "terse version" for lectures and a "full version" with much more text that can be read carefully outside of class and used as a template for homework assignments.
Some fundamental themes of the course...
- 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.
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.
Coq runs on both Windows and pretty much all flavors of
Unix (including Linux and OS X). You will need:
- 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.
A tar file containing the full sources for the notes (as a
collection of Coq scripts and HTML files) is available here:
- http://www.cis.upenn.edu/~bcpierce/sf
The current version of the notes has been developed over the past
two years, in courses at Penn, San Diego, Baltimore, and Portland
State. We believe the flow of ideas is now pretty smooth and the
notes overall are ready for test driving by brave souls elsewhere,
but many rough edges remain. Some of the most serious:
- The first few chapters include quite a bit of text, but it gets a little more sparse later in the course. Even in the early chapters, the level of polish is nowhere near textbook standards.
- The terse versions of most chapters are skeletal -- they contain just bare Coq code and still need to be annotated with "talking points" for lectures.
- We include informal "paper proofs" to accompany many of the formalized proofs, so that students can begin to get a feel for moving between these levels. But there aren't enough, and the ones that are there are mostly not very beautiful.
- The use of Coq is probably not as elegant as it could be.
- The generated HTML files are not very pretty.
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.
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.