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
    • theory of subtyping

Looking Forward

Some good places to go for more...
  • 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 Castéran. Springer-Verlag, 2004.