Postscript.v

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