Recent developments in Type Theory

Lectures at Mathematical Structures of Computation - Lyon 2014

Hugo Herbelin and Danko Ilik

Lecture 1. Constructive proofs in continuation passing style (CPS). The case of completeness of intuitionistic logic w.r.t. Kripke models

14/01/2014 -- Danko

The purpose of this lecture was to show that CPS can also be useful for writing proofs in intuitionistic logic. CPS is a technique of general interest, not exhausted by the connection to double-negation translations -- it is most useful if combined with other computational side-effects besides continuations, like the exception monad (corresponding to logical A-translation) and state/reader monad. In this lecture, we illustrated the technique on the problem of completeness of Kripke models.

We used the Agda proof assistant, and gave a homework to do using it. If you would like do it, but are having trouble installing Agda, we prepared for you a custom ISO image of Debian linux with Agda preinstalled, which you can copy on a USB stick and boot up from, or run in a virtual machine (using VirtualBox, Gnome Boxes, VmWare, ...).

Files from the lecture:

Homework:

  1. Extend KripkeCompletenessCPS.agda for conjunction. You may first want to do it inside KripkeCompleteness.agda.
  2. Extend KripkeCompletenessCPS.agda with a zero, successor and recursor (at higher types), obtaining NBE for Gödel's System T with sum types.

Lecture 3. Reifying CPS proofs: direct style constructive systems based on delimiting control operators and their meta-mathematical properties

16/01/2014 -- Danko

Gödel's System T extended with shift and reset at natural numbers as computational core. Constructive extension of the natural deduction system for minimal intuitionistic logic with shift and reset at a Sigma-0-1 formula, and their properties. Proofs of Markov's Principle and the Double Negation Shift, and their meta theoretical status. Formal Church's Thesis. Issues with the Axiom of Choice. There is no homework, but you can look at the following material:
  1. Normalization of System T with shift and reset in Coq -- systemt-reset-nbe.zip -- works, but code is not as clean as the version without natural numbers
  2. Herbelin's article An intuitionistic logic that proves Markov's principle
  3. Ilik's article Delimited control operators prove Double-negation Shift
  4. The manuscript Double-negation shift as a constructive principle, for connections to Church's Thesis, Choice, and Dialectica -- WARNING: the remarks regarding LPO are wrong, and the proof of constructivity of HA+DNS+AC is not complete (although for HA+DNS it holds).

Lecture 4. Generalizing proving with control to proving with effects. Monotone memory access simplifies Kripke and Gödel's completeness proofs. Direct proof of Open Induction on Cantor Space using delimited control.

17/01/2014 -- Danko

General comments on the constructivity of the completeness proof for classical first-order logic. Some motivation for treating other computational effects in logic, besides control operators. Veldman's proof of the Open Induction Principle on Cantor space using delimited control operators.
  1. You may look at the manuscript A Direct Constructive Proof of Open Induction on Cantor Space and the associated Coq formalization of the proof.
Back to Danko's home page