Ämnesdisposition

  • Allmänt

    Over all motivation and description

    Modern type theory is a logical theory that has dual roles as a foundational system for mathematics, on the one hand, and as a (theoretical) programming language, on the other. Type theory is widely used in computer science in formal verification of systems and programs, and also for constructing large scale formal proofs in mathematics. The theory is ideally suited as a foundation for constructive mathematics, and in fact, proving a theorem in theory is the same thing as constructing a program that computes what the theorem says exists. This can been seen in semi-automated proof support systems as Coq and Agda which will be used during the course. Type theory is also the background for the novel developments in homotopy theory and univalent foundations by Voevodsky and his group.

    The course deals to a large extent with theoretical questions regarding type theory. Thus it will start with fundamental notions such as simple types, lambda-calculus, reduction rules, confluence and normalization, and then go on to more advanced theories with dependent types (Martin-Löf type theory) and the notions particular to that, such as contexts, judgments forms, inductive types, type universes, and their semantics, both informal and formal.

    Aim of the course

    The student should be able to define the basic notions and derive the first properties in lambda calculus and type theory, and should be able to explain and prove fundamental theorems about type theory and its semantics. Another important skill to be acquired is how to use type theory to formalize and prove theorems in mathematics, and with the help of that extract algorithmic content from proofs.

    Teacher:
    Erik Palmgren

    Time and place:
    The lectures will be held on Mondays from 10:15 to 12:00 and Thursdays from 15:15 to 17:00, starting 4 November, in room 306, house 6, Kräftriket (Roslagsvägen 101).



    Schedule

    References

    Course litterature

    P. Martin-Löf, Intuitionistic type theory. Notes by Giovanni Sambin of a series of lectures given in Padua 1980. Bibliopolis 1984. Out of Print. Electronic version available here.

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

    Articles about lambda-calculus and models of type theory:  Distributed during the course.

    H.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


    Reference litterature

    Homotopy Type Theory: An Introduction to Univalent Foundations, Institute of Advanced Study 2013. Open access E-book available here.

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

    P. 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.

    B. Nordström, K. Peterson and J.M. Smith. Programming in Martin-Löf's Type Theory: An Introduction. Oxford University Press, Oxford 1990. Out of Print. Open access E-book available here.

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

    Software

    The Coq proof assistant, documentation and tutorials can be found here

    Examination and Grading


    The examination will consist in four hand-in problems, and an oral examination. If you wish to take the course as a PhD-course, an extra project or seminar will be required.

    Problem set   Date of issue and hand-in    Maximum score
    1 14 Nov. -  28 Nov. 20
    2 28 Nov.  - 12 Dec. 20
    3 5 Dec.   -  20 Dec. 30
    4 12 Dec   - 9 Jan. 30

      

    Grade Requirements
    A  90-100 points + oral exam
    B  80-100 points + oral exam
    C  60-79 points
    D  50-59 points
    E  45-49 points
  • Lecture 1

    Historical introduction. BHK-interpretation. Judgements in logic and Martin-Löf type theory.

  • Lecture 2

    Meaning explanations of the judgement forms. Canonical elements. Hypothetical judgements and their meaning. Equality and substitution rules. Abstract computation relations. Lazy evaluation.

    (Lecture on November 8 was cancelled.)

  • Lecture 4

    Type-theoretic axiom of choice. Binary sums and empty types. Simple inductive types. Finite sets. Natural numbers

  • Lecture 5

    Using primitive recursion to define arithmetical functions. 

    Introduction to the proof assistant Coq. GALLINA specification language and type theory: products, inductive types, definitions and theorems, eval-compute. Simple tactics.

  • Lecture 6

    Identity types and equivalence relations. Setoids. Extensional functions. Choice principle: type-theoretic axiom of choice, Zermelo's axiom of choice, axiom of unique choice. 

  • Laboration

    Bring laptop - we will do Exercises 2 and parts of Yves Bertot's tutorial Coq in a Hurry (coq.inria.fr).

  • Lecture 7

    Well-founded relations. Well-orders. Complete induction on N. Transitive closure. W-types. Brouwer's second number class. Immediate subtree relation on W-type is an example of a well-founded relation.

  • Lecture 8

    Type universes. Reflection. Universes as sets of truth-values. Propositional functions and restricted power sets. Aczel's set of iterative sets. Bisimulation. Universes in Coq: impredicativity of Prop. True power sets. Weak existential quantifiers, and their reduction to Pi-types using Prop.

  • Lecture 9

    Setoids and extensional functions form category. Quotient setoids and subsetoids. Products and sums of setoids. Identity types and free setoids. Finite and finitely enumerable setoids.

  • Lecture 10

    Diaconescu's theorem for setoids. Countable and uncountable setoids.

    The type theory behind Coq: inductively defined families, arities, strictly postive occurence, constructor forms, general elimination rules. (Christine Paulin Mohring: Inductive Definitions in the System Coq: Rules and Properties. ENS Lyon, L.I.P. Research Report 92-49, 1992.  See also Coq Reference Manual Chapter 4.) 

  • Lecture 11

    Normalization proofs and termination problems: Pure untyped lambda-calculus. Strong normalization for simply typed lambda-calculus (Lambda->Curry). We followed:

    H.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

    • Lecture 12 (Friday December 20)

      Explicit substitution and models of Martin-Löf type theory

      • Lecture 13 (January 9)

        Models of Martin-Löf type theory, continued.

      • Presentation of projects (15 January)

        Presentation of projects in room 16 building 5, 10.15 -- 16.00.

        Schedule:

        10.15 - 10.45 Anders Lundstedt  (Ramsey Theory in Coq)

        10.55 - 11.25 Oliver Krüger (Normalization of Gödel's T)

        11.35 - 12.05 Alex Loiko (Buchberger algorithm in Coq)

        13.15 - 13.45 Håkon Robbestad Gylterud (Constructive set theory in Agda)

        13.55 - 14.25 Mattias Granberg Olsson (Group actions in Coq)
         
        14.35 - 15.05 Nick Andersson (Formalisation of Gödel's ontological proof of God)

        15.15 - 15.45 Jonne Mickelin Sätherblom (Coinduction)