IMC027 Advanced Lambda Calculus
Lectures: Monday 10:45 12:30
Weeks: 3542, 4550, 12
Room: HG 01.029
1)  13 Sept. SLIDES 
Topics: Untyped λcalculus, βreduction graph [Bar92, pag. 28], Church numerals,
encoding of Booleans, λdefinition of ifthenelse, encoding of tuples, BohmPipernoGuerrini's encoding of datastructures [BarDS10, Ch 6],
selfinterpreter 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 selfinterpreter 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, wellfounded
order on finite multisets, Abstract Reduction System (ARS),
being and having a normal form, weak normalization, strong
normalization, confluence (ChurchRosser), 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, Nonreducibility, Hierarchy Theorem Revisited 

Last update: 25 November 2010