Coq School 2013, Tsinghua

Jean-Jacques Lévy ( Tsinghua, 2013 )

  • 5th Asian-Pacific Summer School on Formal Methods (August 5-10, 2013) (see web site for full program)
      Class 1 Functions [Pdf, Pdf4]

      Class 2 Data types (I) [Pdf, Pdf4]

      Class 3 Data types (II) [Pdf, Pdf4]

      Class 4 Polymorphism [Pdf, Pdf4]

  • Several references
      Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions.
      Yves Bertot, Pierre Casteran. Springer, pp. 497, 2004. ISBN: 978-3642058806.

      Bibliography on lambda-calculus
      Lambda-calculus and Programming (in French) [Pdf, Video]

  • Course, Tsinghua University, Beijing, 2013