## 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

 [BarDS10] Henk Barendregt, Wil Dekkers and Richard Statman. Lambda calculus with types. (new Barendregt's book) [Bar84] Henk Barendregt. The lambda calculus. Its syntax and semantics. Studies in Logic and the Foundations of Mathematics, Volume 103, North-Holland, 1984. (old Barendregt's book) [Bar92] Henk Barendregt. Lambda calculi with types, in Handbook of Logic in Computer Science, 1992.

Last update: 25 November 2010