Lambda-Calculus

Jean-Jacques Lévy ( Tsinghua, August-September 2010 )

  • 2 talks at the 2nd Asian-Pacific Summer School on Formal Methods (23-24 August)
      Class 1 Lambda notation, computation models. [Pdf, Pdf4]
      Class 2 Confluency, finite developments, standardization [Pdf, Pdf4]

  • More advanced course (3-18 September, agenda)
      Class 3-1 Reminders, local confluency, confluency, residuals. [Pdf, Pdf4]   Exercices [Pdf, Pdf4]
      Class 3-2 Residuals. Finite developments. Parallel moves. Cube lemma. [Pdf, Pdf4]
      Class 3-3 Normalization, strong normalization. Standardization [Pdf, Pdf4]

      Class 3-4 Lambda-theories. Bohm theorem. Head normal forms. Bohm trees. [Pdf, Pdf4]
      Class 3-5 Continuity theorem. Observational equivalences. Extensionality. [Pdf, Pdf4]
      Class 3-6 Bohm trees and Scott's models [Pdf, Pdf4]

  • Several references
      Bibliography
      Lambda-calculus and Programming (in French) [Pdf, Video]

  • Course, Tsinghua University, Beijing, 2010