Ämnesdisposition

  • Type theory VT23

    Fäll ihop allt Expandera allt

    OBS: first lecture 23/1, not 16/1 as originally scheduled.

    Overall motivation and description

    Type theories are a range of logical systems that can play dual roles: as a foundational systems for mathematics, on the one hand, and as a (theoretical or real-world) programming languages, on the other. Mathematically, the theory is ideally suited as a foundation for constructive mathematics: proving a theorem in type theory is the same thing as constructing a program that constructs/computes the objects whose existence is asserted by the theorem. On the other hand, computer implementations of type theory are now widely used for formal verification of systems and programs, and also for computer-formalization of large-scale mathematical proofs.

    This course will aim to overview various aspects of type theories: introducing them as a formal systems, starting with simple type theory and building to dependent type theory; developing some basic mathematics inside these systems; studying their models and proof-theoretical properties; and exploring their computer implementations, including Haskell and Coq.

    Aim of the course

    Students should understand the basic notions and formal rules of simple and dependent type theories, understand how to use them to write programs and state and prove mathematical definitions and theorems, both by hand and in computer implementations, and understand the Curry–Howard correspondence between proofs/definitions and programs.

    Lecturer:
    Peter LeFanu Lumsdaine (p.l.lumsdaine@math.su.se)

    Time and place:
    The lectures will be held on Mondays, from 13:00 to 15:00, starting on 23 January, in irregular locations in Albano/Frescati (sorry!). OBS: course start is delayed one week from the original schedule, to avoid an exam clash; an extra lecture will be scheduled later in the term as replacement.

    Full schedule on TimeEdit

    Evaluation and grading

    By final project (topic list and further details below) and optional homeworks.

    Literature

    Core texts

    P. Martin-Löf, Intuitionistic type theory: Notes by Giovanni Sambin of a series of lectures given in Padua 1980, Bibliopolis 1984 (usually known as “the Bibliopolis book”). Out of print; electronic version available from here.

    B. Nordström, K. Peterson and J.M. Smith, Programming in Martin-Löf's Type Theory: An Introduction, Oxford University Press, Oxford 1990. Pdf available here.

    R. Harper, Practical Foundations of Programming languages, Cambridge University Press 2016, available online from Harper’s homepage and the SU library

    Supplementary resources

    Learn You a Haskell for Great Good (Haskell tutorial)

    Homotopy Type Theory: An Introduction to Univalent Foundations (aka the HoTT Book), the Univalent Foundations Program, 2013.

    Henk P. Barendregt, Lambda-calculus with types. In: (S.\ Abramsky and T.S.E. Maibaum eds.) Handbook of Logic in Computer Science vol. 2, Oxford University Press 1992.  PDF

    Martin Hofmann, Syntax and Semantics of Dependent Types, in: Sematics and Logic of Computation. Cambridge University Press 1997. E-book and  PDF. 

    Erik Palmgren, Lecture notes on type theory, 2014. PDF.

    Per Martin-Löf, On the Meanings of the Logical Constants and the Justifications of the Logical Laws, Nordic Journal of Philosophical Logic, 1(1): 11–60, 1996. PDF.

    Aarne Ranta, Type Theoretical Grammar, Oxford University Press, Oxford, 1994.

    Software

    Haskell (programming language)

    Coq (proof assistant)

    Agda (proof assistant)


  • Simply-typed λ-calculus

    • Recall: first-order logic, algebraic logic over a signature
    • Simply-typed λ-calculus over a signature
    • Abstract characterisation of syntax via inductive universal property
    • Standard interpretation of STλC as sets, functions
    • Implementation in Haskell
    • Parametricity for STλC

    Selected resources, exercises to come soon.

  • Untyped λ-calculus

    • Syntax of untyped λ-calculus
    • Reduction relations
    • Church encoding of naturals, booleans; recursive functions
    • Normal forms, reduction strategies
    • Church–Rosser; weak normalisation
    • Strong normalisation

    Recommended resources:

    • Barendregt Lambda calculi with types, §2 (pdf linked above in course literature)

  • Reduction in typed theories

    • Reduction relations in simply typed lambda-calculus
    • Strong normalisation (using Harper’s version of Tait’s method, roughly following Angiuli 2015, How to prove STLC is normalising)


  • Exam project topics