IMC027 Advanced Lambda Calculus
Lectures: Monday 10:45 12:30
Weeks: 35-42, 45-50, 1-2
Room: HG 01.029
| 1) | 13 Sept. SLIDES |
Topics: Untyped λ-calculus, β-reduction graph [Bar92, pag. 28], Church numerals,
encoding of Booleans, λ-definition of if-then-else, encoding of tuples, Bohm-Piperno-Guerrini's encoding of data-structures [BarDS10, Ch 6],
self-interpreter and enumeration [BarDS10, Ch 6]. Homeworks: Write the β-reduction graphs of the examples in the slides. Define lists of natural numbers, encode them, λ-define the append. Check that the self-interpreter actually works. |
| 2) | 20 Sept. |
Topics: Simple Types, notations on types, notions of order and rank. Simply Typed Lambda Calculus (à la Curry and à la Church), β and η-reductions. Properties: substitution lemma, subject reduction. Equivalence of the systems: forgetful map, preservation of typable terms, preservation of types under reduction. Definitions of normal forms and characterization of β-normal forms. Everything is in [BarDS10, Ch 1] |
| 3) | 27 Sept. |
Topics:. Long normal forms, inhabitation machines (both
for lnf and βnf), definition of multiset, well-founded
order on finite multisets, Abstract Reduction System (ARS),
being and having a normal form, weak normalization, strong
normalization, confluence (Church-Rosser), Levy's lemma about
characterization of creation of redexes.
Everything is in [BarDS10, Ch 1, Ch 2] |
| 4) | 04 Oct. SLIDES |
Topics:Variants of simply typed lambda calculus,
semantics, observational equality, type strutures |
| 5) | 11 Oct. SLIDES |
Topics: Various Type Systems, (full) Type Structures,
semantics, partial semantics, typed lambda models, Five Easy
Pieces, observational equivalence, logical relation, extensional
equivalence. |
| 7) | SLIDES |
Topics: Five Easy Pieces, Type Reducibility, Positive and
Negative subtype occurrences, type hierarchy, adding constants. |
| 8) | SLIDES |
Topics: Type Reducibility |
| 9) | SLIDES |
Topics: Term models, Non-reducibility, Hierarchy Theorem Revisited |
|
Last update: 25 November 2010