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]