Postscript
(* $Date: 2011-04-10 12:14:37 -0400 (Sun, 10 Apr 2011) $ *)
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.