Lectures

Thorsten Altenkirch
Towards a syntax for cubical type theory

One of the key problems of Homotopy Type Theory is that it introduces axioms such as extensionality and univalence for which there is no known computational interpretation. We propose to overcome this by introducing a Type Theory where a heterogenous equality is defined recursively and equality for the universe just is univalence. This cubical type theory is inspired by Bernardy and Moulin's internal parametricity and by Coquand, Bezem and Huber's cubical set model. This is ongoing work with Ambrus Kaposi at Nottingham.

Timothy Gowers (University of Cambridge)
Fully automatic problem solving with human-style output

I shall describe a program that Mohan Ganesalingam and I created that proves simple statements in elementary abstract analysis. I shall also discuss the broader project of which this is intended to be just a preliminary step. Briefly, the aim is to write a series of programs that solve problems in a “fully human” way, meaning that they do not undertake any search that a human mathematician would not consider undertaking. At first, this seems to be sacrificing everything that makes a computer worth using. However, I shall attempt to explain why we regard this view as mistaken.

Jean-Louis Krivine
50 years after forcing, Curry-Howard correspondence gives new models of ZF

Classical realizability appeared as a method to extend the proof-program correspondence to the whole of ZF set theory, even with DC (dependent choice). As a by-product, it gives completely new models of ZF + DC, that we shall consider in these talks. The method of forcing is indeed a (very) particular case, that we shall avoid, of course.

The principal tools are :

i) A conservative extension of ZF, called ZF_epsilon, with a new strong membership relation, which does not satisfy extensionality.

ii) The structure of realizability algebra, which is a three-sorted extension of the well known combinatory algebra of Curry.
The ordered sets of conditions, used in forcing, are degenerate cases of realizability algebras. he usual models of lambda-calculus (stable spaces, hypercoherence spaces, …) are examples of realizability algebras.

The models of ZF obtained in this way are much more difficult to study than the ordinary forcing models: they are not extensions of the ground model, ordinals and even integers are not preserved and neither is the axiom of choice. I shall explain what we already know about their structure. We shall look at some examples, which give some new relative consistency results, with DC and R not well ordered.

Up to now, there are few such new results, even though the method is much more general than forcing. The reason is, of course, that we do not yet understand sufficiently well the structure of these models.

François Pottier
The practice and theory of Mezzo

The programming language Mezzo is a member of the ML family, from whom it inherits algebraic data types, first-class functions, and automatic memory management. It is equipped with a rich type system that controls aliasing and access to mutable memory. This static discipline rules out certain programming mistakes, guarantees data race freedom, and opens up some new possibilities, such as gradual initialization and type(state) changes. In the first lecture, I will present Mezzo via a series of examples. In the second lecture, I would like to present the meta-theory of Mezzo. It is organized in a modular manner and has been machine-checked in Coq.

Olivier Serre
Tree Automata, Logic and Verification of (Higher-Order-) Functional Programs

The first goal of these two lectures is to introduce the audience with tree automata and their connections with model checking of various logic (with a special focus on monadic second order logic). In particular we will explain why these two formalisms are equi-expressive when describing sets of trees.

In a second part we will explain how a higher-order recursion scheme (a kind of term rewriting system) can be used to model the behaviour of a higher-order functional program by generating (assuming some restriction on the program) its syntax tree.

Finally we will combine these two concepts, automata/logic and higher-order recursion schemes, and argue that they can successfully be used to solve important questions related to verification of programs, in particular the model-checking problem (both local and global) as well as the synthesis problem.

Note: the slides of the two lectures are available here and here.

Bruno Vallette (Université Nice Sophia Antipolis)
Théorie de la déformation des algèbres de Batalin—Vilkovisky

La notion d’algèbre de Batalin—Vilkovisky est assez élémentaire : algèbre commutative munie d’un opérateur différentiel d’ordre 2 et de carré nul. Elle apparait aujourd’hui en algèbre (algèbres vertex), géométrie (variétés de Frobenius), topologie (topologie des cordes) et physique mathématique (renormalisation).

Le but de ces exposés sera d’établir la théorie de la déformation des algèbres de Batalin—Vilkovisky (BV). Pour cela, nous aurons besoin de plusieurs outils, que nous rappellerons : une opérade qui code la catégorie de algèbres BV, une bonne résolution de cette opérade (la résolution de Koszul et le modèle minimal), et enfin, une algèbre de Lie qui code les déformations de structures d’algèbres BV.

Au final, cette théorie permettra de résoudre plusieurs conjectures : celle de Lian—Zuckerman sur les algèbres vertex et celles de Kontsevich sur l’action du groupe de Givental, par exemple.