#
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