IMC027 Advanced Lambda Calculus
Lectures: Monday 10:45 12:30
Weeks: 35-42, 45-50, 1-2
Room: HG 01.029
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.
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]
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]
Topics:Variants of simply typed lambda calculus,
semantics, observational equality, type strutures
Topics: Various Type Systems, (full) Type Structures,
semantics, partial semantics, typed lambda models, Five Easy
Pieces, observational equivalence, logical relation, extensional
Topics: Five Easy Pieces, Type Reducibility, Positive and
Negative subtype occurrences, type hierarchy, adding constants.
Topics: Type Reducibility
Topics: Term models, Non-reducibility, Hierarchy Theorem Revisited
Last update: 25 November 2010