Advanced Lambda Calculus (2010-2011) IMC027


Teachers:
Henk Barendregt x.henkxcs.ru.nl)@
Giulio Manzonetto x.gmanzonexdsi.unive.it)@

Details

IMC027 Advanced Lambda Calculus
Lectures: Monday 10:45 12:30
Weeks: 35-42, 45-50, 1-2
Room: HG 01.029

Topics of the Course

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

Useful Material

Last update: 25 November 2010