From January 13 to January 17 at the Université Lyon 1.
Amphitheatre of the Polytech'Lyon building, tramway T1 or T4, stop “Condorcet” or “Université Lyon 1”.

• Prelude to Continuations
  • Olivier Danvy, University of Aarhus, Denmark.
  • Chung-Chieh Shan, Indiana University, USA.
  • Slides and source files

• Proving with side effects: a few examples
  • Hugo Herbelin, INRIA, Université Paris 7.
  • Danko Ilik, INRIA.

• Homotopy Type Theory and Univalent Foundations
  • Nicola Gambino, University of Leeds, United Kingdom.
  • Dan Licata, Wesleyan University, USA.
  • Peter Lumsdaine, Dalhousie University, Canada.
  • Slides: Lecture 1 Lecture 3 Lecture 4

• Thorsten Altenkirch, University of Nottingham, United Kingdom.
• Federico Aschieri, ÉNS Lyon, France. Slides
• Guillaume Brunerie, ÉNS Paris, France.
• Eric Finster, PPS lab, France
• Richard Garner, Macquarie University, Australia.
• Alexander Kreuzer, ÉNS Lyon, France. Slides
• Paul-André Melliès, PPS lab, France.
• Alexandre Miquel, Universidad de la República, Montevideo, Uruguay. Slides
• Nicolas Tabareau, INRIA, Nantes, France.
• Michael Warren (cancelled)

Homotopy type theory (HoTT) enriches the correspondence type/formula and proof/program into a correspondence type/space, and interprets the equality type of proofs of Martin-Löf theory in terms of homotopy. The modelisation of type theory into simplicial spaces has suggested the adjunction of a new axiom of univalence (Voevodsky), relating equality with homotopy equivalence, opening the door to a constructive formalisation of homotopy theory.

The extension of the Curry-Howard isomorphism to effects is a natural continuation of the discovery of the correspondence between control operators (call-cc) and classical logic (Griffin) and of the consideration of the polarities in logic (Girard). This research direction aims at the exploration of extensions of type theories with effects, in direct style, towards an enrichment of its expressivity.

This week will consist of morning lectures (in a winter school-style) and afternoon workshop-style invited talks.

• Pierre-Louis Curien, CNRS, Université Paris 7,
• Hugo Herbelin, INRIA, Université Paris 7.

Olivier Danvy, Chung-Chieh Shan
Prelude to Continuations

Lecture #1: Identifying control
Outline: How continuations arise in functional programming
Tagline: “Speculation is an essential creative activity.” – Alexander Grothendieck

Lecture #2: Representing control
Outline: The transformation into continuation-passing style (CPS) of terms and types, and its logical counterpart
Tagline: “CPS is everywhere.” – Pierre-Louis Curien

Lecture #3: Exercising control
Outline: Defunctionalization and its application to abstract machines, quantification in natural language, and probability measures
Tagline: “A mathematician is expected to sit at his computer and think.” – Hari Seldon

Lecture #4: Delimiting control
Outline: The hierarchy of control induced by repeated CPS transformation
Tagline: “These continuations have continuations.” – Peter J. Landin

Hugo Herbelin, Danko Ilik
Two case studies in proving with side-effects: Gödel's and Kripke's completeness theorems

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

Lecture 2: The case of Gödel's completeness proof of classical logic w.r.t. Boolean models.

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

Lecture 4: Generalizing proving with control to proving with effects. Monotone memory access simplifies Kripke and Gödel's completeness proofs.

Link to Danko Ilik's course material.

Nicola Gambino, Dan Licata, Peter LeFanu Lumsdaine
Homotopy Type Theory and Univalent Foundations

The aim of these lectures is to give an introduction to the area of Homotopy Type Theory and to Voevodsky’s Univalent Foundations Programme, which seeks to develop new foundations of mathematics on the basis on type theories extended with axioms inspired by homotopy theory.

Plan:

Lecture 1. Review of type theory, main metamathematical properties
Lecture 2. The homotopy-theoretic model of type theory
Lecture 3. The Univalence Axiom
Lecture 4. The computational interpretation of the Univalence Axiom
Lecture 5. Higher inductive types and examples of homotopy theory in type theory
Lecture 6. Agda/Coq formalizations

Thorsten Altenkirch
Containers in Homotopy Type Theory

We explore the notion of container (i.e. strictly positive datatypes) in the context of Homotopy Type Theory (HoTT). It turns out that containers give rise to a much richer notion of datatypes in this setting, including multisets and “rings” (a list without a beginning). Based on previous work by Gylterud we can show that all containers whose shapes are sets have an antiderivative (this fails in ordinary type theory). However, the question wether all containers have antiderivatives in HoTT appears to be open.

Federico Aschieri
Realizability and learning in classical Arithmetic

Classical proofs do not yield perfect constructive information about the statements they prove. In other words, they do not contain a winning strategy, that is, a method of answering every question an opponent can make about the proven statement.

What do we do in real life when we have to play in a game, but we do not know any winning strategy? Well, rather than paralyze ourselves, we do play nonetheless. What we do, in particular, is to play at our best, at the best of our current knowledge of the game. And strong players take each defeat as a lesson, as an opportunity to improve their knowledge of the game and therefore their ability. They learn by interaction.

In the young theory of Interactive realizability classical proofs are interpreted the same way. One interprets a proof as a player/program, who maintains a well-structured set of hypotheses, information, knowledge, and use it to answer opponents' questions. Each time the players fails to provide a correct answer, he is able to automatically learn new things and to improve their knowledge and their strength. In many case this learning process stops, and the player is finally able to answer correctly the opponent's question. The goal of this talk is to introduce this theory of realizability.

Guillaume Brunerie
Cubical homotopy type theory

In this talk I will present some work in progress on a cubical syntax and typing rules for homotopy type theory. The ultimate goal is to get a type theory without axioms, suitable for homotopy type theory (i.e. where universes are univalent and higher inductive types are built-in to the theory), which can be implemented in a proof assistant and satisfying good metatheoretical properties like decidability of type checking, canonicity and strong normalisation.

This work in progress is based on some previous work on the computational interpretation of homotopy type theory together with Carlo Angiuli, Robert Harper and Dan Licata, and is inspired by Thierry Coquand’s and Simon Huber’s work on a cubical set model of HoTT.

Eric Finster
Opetopic Diagrams as a Language for Higher Categorical Proofs

The Opetopes are a set of higher-dimensional tree-like polytopes first defined by Baez and Dolan for the purpose of defining weak higher categories. Presheaves on the category of opetopes (the opetopic sets) form a subcategory of all polygraphs (or computads), and we can identify weak omega-categories  in this subcategory using a lifting property (somewhat analogous to the Kan  condition for simplicial sets) due to Thorsten Palm.

The tree-like structure of these shapes provides a natural interpretation  of the aforementioned lifting property in terms of a diagrammatic syntax  which is easily implemented by computer, leading to a kind of diagrammatic proof assistant for deriving and manipulating higher categorical cells.

In this lecture I will give an overview of the diagrammatic calculus and demonstrate a prototype implementation.

Richard Garner
Further thoughts on coherence issues in dependent type theory

A well-known problem for the categorical interpretation of dependent type theory is that in typical semantic models, the natural substitution operation fails to be as strict as the syntax requires it to be. Most solutions that have been proposed to this problem involve “strictification”: replacing the semantic models at issue by equivalent strict ones. A notable exception is an approach suggested by Curien, in which the notion of type theory is expanded to allow for explicit “substitution up to isomorphism”; then the semantic models of interest are direct instances of this structure. In this talk, we look at Curien's approach from the perspective of two-dimensional monad theory. More precisely, we will describe a monad on a presheaf category whose algebras are type theories, and how how to lift this to a 2-monad on a presheaf 2-category amongst whose pseudoalgebras are numbered the semantic models of interest.

Alexander Kreuzer
Program extraction and higher order reverse mathematics

Reverse mathematics is a program which tries to determine which set-existence axioms are needed to prove theorems in mathematics. For instance, it was shown that the Bolzano-Weierstrass principle requires arithmetical comprehension (and is in fact equivalent to this), see e.g. [1]. Usually, this investigation are done in fragments of so-called second order arithmetic which is actually a two-sorted first order theory with a type for natural numbers and a type for sets of natural numbers. Kohlenbach introduce a finite-type extension of this system, see [2].

In this talk we will introduce reverse mathematics and this higher order extension. We will present program extraction techniques based on Gödel's functional interpretation. Using this we will analyze higher order statements like the existence of a non-principal ultrafilter or the existence of the Lebesgue measure on all subsets of the unit interval.

Paul-André Melliès
An environment-friendly tensorial logic

Alexandre Miquel
Implicative algebras for noncommutative forcing (or: doing realizability without realizers)

In this talk I shall present work in progress about the connections between Cohen's forcing and Krivine's classical realizability, in the perspective of comparing the corresponding models for set theory.

First, I will introduce a very general a simple poset structure - the notion of implicative algebra - that subsumes complete Boolean algebras (underlying the construction of forcing models) as well as Krivine's classical realizability algebras. I will show how in this structure - that provides no primitive notion of a realizer - we can reconstruct realizers from truth values (now seen as the primitive notion) and reduce the realizability relation to subtyping (seen as primitive). I will conclude this part of the talk by showing that implicative algebras are essentially a realizer-free presentation of Krivine's realizability algebras, by defining a categorical equivalence between the triposes induced by both structures.

In the second part of the talk, I will show how implicative algebras can be used to factorize the construction of Boolean-valued models and classical realizability models of set theory, while subsuming the corresponding correctness/adequacy results. Using this, I will describe the global structure of the models of set theory induced by classical realizability, while comparing it with the much more simple structure of forcing models. Finally, I will present and discuss some of the important open questions that are naturally raised by the comparison of both kinds of models.

Nicolas Tabareau
The sheaf construction in Homotopy Type Theory

We present how the shift from Type Theory to Homotopy Type Theory and in particular the introduction of the univalence principle allows to internalize the sheaf construction (à la Lawvere-Tierney) inside Type Theory. In particular, we show that the sheaf construction provides a complete negative translation of Homotopy Type Theory in the style of Gödel translation from classical logic to intuitionistic logic. We will discuss the computational content of this translation.