Postscript
(* $Date: 2013-01-28 08:53:29 -0500 (Mon, 28 Jan 2013) $ *)
Looking back...
- Functional programming
- "declarative" programming (recursion over persistent data
structures)
- higher-order functions
- polymorphism
- Coq, an industrial-strength proof assistant
- Logic, the mathematical basis for software engineering:
logic calculus -------------------- = ---------------------------- software engineering mechanical/civil engineering
- inductively defined sets and relations
- inductive proofs
- proof objects
- Foundations of programming languages
- notations and definitional techniques for precisely specifying
- abstract syntax
- operational semantics
- big-step style
- small-step style
- type systems
- Hoare logic
- program equivalence
- fundamental metatheory of type systems
- progress and preservation
- progress and preservation
- theory of subtyping
- notations and definitional techniques for precisely specifying
Looking Forward
- Several optional chapters of Software Foundations
- Cutting-edge conferences on programming languages:
- POPL
- PLDI
- OOPSLA
- ICFP
- (and many others)
- More on functional programming
- Learn You a Haskell for Great Good, by Miran Lipovaca (ebook)
- and many other texts on Haskell, OCaml, Scheme, Scala, ...
- More on Hoare logic and program verification
- The Formal Semantics of Programming Languages: An Introduction, by Glynn Winskel. MIT Press, 1993.
- Many practical verification tools, e.g. Microsoft's
Boogie system, Java Extended Static Checking, etc.
- More on the foundations of programming languages:
- Types and Programming Languages, by Benjamin C. Pierce. MIT Press, 2002.
- Practical Foundations for Programming Languages, by Robert Harper. Forthcoming from MIT Press. Manuscript available from his web page.
- Foundations for Programming Languages, by John C. Mitchell.
MIT Press, 1996.
- More on Coq:
- Certified Programming with Dependent Types, by Adam Chlipala. A draft textbook on practical proof engineering with Coq, available from his web page.
- Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions, by Yves Bertot and Pierre Casteran. Springer-Verlag, 2004.
- Iron Lambda (http://iron.ouroborus.net/) is a collection of Coq formalisations for functional languages of increasing complexity. It fills part of the gap between the end of the Software Foundations course and what appears in current research papers. The collection has at least Progress and Preservation theorems for a number of variants of STLC and the polymorphic lambda-calculus (System F)