Preface

(* Preface
   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.

Overview


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

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

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

  • 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


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.

System Requirements


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.

Access to the Coq files


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

State of Play


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.

For Instructors


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.