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
    • type soundness for languages with dynamically allocated heap storage
  • theory of subtyping

Further Reading

• Types and Programming Languages, by Benjamin C. Pierce. MIT Press, 2002.
  • Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions, by Yves Bertot and Pierre Castéran. Springer-Verlag, 2004.
  • Certified Programming with Dependent Types, by Adam Chlipala. A draft textbook on practical proof engineering with Coq, available from his web page.
  • Practical Foundations for Programming Languages, by Robert Harper. Manuscript, available from his web page.
  • The Formal Semantics of Programming Languages: An Introduction, by Glynn Winskel. MIT Press, 1993.
  • Foundations for Programming Languages, by John C. Mitchell. MIT Press, 1996.