Types logo, by Florent Kirchner

Program of the Workshop

Invited Talks

Richard Garner: Topological and higher-dimensional aspects of type theory

It was observed by Hofmann and Streicher in the 1990s that, in Martin-Löf's intensional type theory, it is possible to endow each type A with a groupoid structure, by taking as the ``type of morphisms'' from a to b, the identity type IdA(a,b). However, it was made clear even at this time that this was not the end of the story. Indeed, the associativity and unitality axioms for this type-theoretic groupoid do not hold on-the-nose, but only up to propositional equality. Thus, if we are to obtain a genuine groupoid from a type, we must first quotient out by propositional equality. A similar phenomenon occurs in the construction of the fundamental group of a topological space: in order that the group operation should be associative on-the-nose, one must quotient out paths by the homotopy relation. This suggests the following analogy: that types are like topological spaces, and that propositional equality is like the homotopy relation. Remarkably, it turns out that this analogy can be made into something precise. The purpose of this talk is to give an overview of the growing body of work which exploits this connection, and to describe some of the challenges that remain.

Pawel Urzyczyn : Decision problems in polymorphic type assignment

This talk will survey known results (some old ones and some new ones) and open questions concerning decision problems related to various type-assignment systems. These decision problems fall into essentially two categories:

  • Typability and type-checking: Given a term M, determine if M can be assigned a given type (or any type at all) in a given (or arbitrary) type environment.
  • Type inhabitation (provability): Given a type t, determine if there is a term M such that M has type t (or equivalently, if t has a proof) in a given type environment.

For the simply typed lambda-calculus, these problems are decidable in polynomial time (type inference) or space (inhabitation). In polymorphic calculi each of them can be undecidable; in particular the famous theorem of Wells states that typability in system F is undecidable. Little is known about decidable subsystems (or variants) of F, for example it is an open problem if typability is decidable in the parametric fragment. In addition to the universal polymorphism of system F and its relatives, this survey will cover the decision problems originating from Curry-style, Church-style and domain-free calculi involving other forms of polymorphism: existential, ad hoc (intersection types) and first-order (dependent types).

Peter Hancock : Entering bars infinitely often

Infinite streams have a natural topology. I'll present a complete representation of continuous functions on streams by data-structures that behave like programs for reading streams and writing values or streams of values. To ensure continuity requires both coinductive and inductive definitions, that on the inductive side, go back to Brouwer's bar-induction. I'll sketch the extension of these ideas to kinds of infinite object more general than streams, where the use of dependent types seems essential.

Joint work with Neil Ghani (Strathclyde) and Dirk Pattinson (Imperial).

Schedule — show all abstracts

May the 11th
19:00 — Cold dinner
May the 12th
09:00 — Registration
12:30 — Lunch
14:00 — Bruno Barras — abstractslides
Extending the Implicit Calculus of Constructions with Union and Subset Types
14:30 — Chantal Keller — slides
Importing HOL-Light into Coq : deep and shallow embeddings of the higher order logic into Coq
Abstract: We present a work in progress that aims at realizing an interface to import HOL-Light theorems into Coq. We propose a deep embedding of the higher order logic into Coq, with data-types representing types, terms and proofs. A translation function lifts these propositions and proofs into their Coq counterparts and is proved correct. In the long run, the main challenge is to have a good representation of HOL data-types, with as compact as possible proofs and a rather fast translation.
15:00 — Lionel Vaux — abstractslides
Primitive recursion in finiteness spaces
15:30 — Coffee Break
16:00 — Cody Roux — abstractslides
Normalisation by set theoretic models and labelling
16:30 — Neil Sculthorpe — abstractslides
Safe Functional Reactive Programming through Dependent Types
17:00 — Denis Cousineau — abstractslides
How to prove strong normalization from weak normalization, the case of minimal deduction modulo
17:45 — Demo session
19:00 — Dinner
May the 13th
09:00 — Pawel Urzyczyn (invited) — abstractslides
Decision problems in polymorphic type assignment
10:00 — Johannes Kanig — abstractslides
Proof of Higher-Order Programs using Effect Polymorphism
10:30 — Coffee Break
11:00 — Jean Duprat — abstractslides
Plane geometry for pupils in Coq
11:30 — Enrico Tassi — abstractslides
Hints in unification
12:00 — Claudio Sacerdoti Coen — abstractslides
Matita NG: reduction and type-checking
12:30 — Lunch
14:00 — Andreas Abel — abstractslides
Normalization by Evaluation for Impredicative Type Theory (Work in Progress)
14:30 — Paola Toto — abstractslides
Algebraic setting for many-valued constructive topology
15:00 — Ugo de Liguoro — abstractslides
An interactive concept of integer and boolean to model classical arithmetic constructively
15:30 — Coffee Break
16:00 — Randy Pollack — abstractslides
A new canonical representation of binding
16:30 — Tom Hirschowitz — abstractslides
Contraction-free proofs and games for Linear Logic
17:00 — Matthieu Sozeau — abstractslides
A New Look at Generalized Rewriting in Type Theory
17:45 — Demo session
19:00 — Dinner
May the 14th
09:00 — Peter Hancock (invited) — abstractslides
Entering bars infinitely often
10:00 — Ioana Pasca — abstractslides
Formal verification of exact computations using Newton\'s method
10:30 — Coffee Break
11:00 — Thorsten Altenkirch — abstractslides
PiSigma a core language for dependently typed programming
11:30 — Hugo Herbelin — abstractslides
Investigations into Kripke models for classical logic
12:00 — Michael Lienhardt — abstractslides
Typing Component-Based Communication Systems
12:30 — Lunch
14:00 — Easy mountain walk
17:00 — Business meeting
19:00 — Dinner
May the 15th
09:00 — Richard Garner (invited) — abstractslides
Topological and higher-dimensional aspects of type theory
10:00 — Zhaohui Luo — abstractslides
Dependent Record Types Revisited
10:30 — Coffee Break
11:00 — Nils Anders Danielsson — abstractslides
Mixing Induction and Coinduction
11:30 — Clement Houtmann — abstractslides
Cut-elimination Canonicity for Classical Sequent Calculus
12:00 — Dulma Rodriguez — abstractslides
Efficient Type-Checking for Amortised Heap-Space Analysis
12:30 — Lunch
14:00 — Damien Pous — abstractslides
Typing and Untyping Various Algebras
14:30 — Francois Garillot — abstractslides
Working effectively with generic subgroups
15:00 — Coffee Break
15:30 — Micaela Mayero — abstractslides
Certification of Numerical Analysis Programs
16:00 — Barbara Petit — abstractslides
A lambda calculus with pattern matching and polymorphims


Humayoun Muhammad
Mathematical Proofs in Natural Languages (MathNat)
Abstract: MathNat is a project for developing tools to enable automatic formalisation of mathematical text.
We proceed in two steps:
  1. Syntax: We develop a controlled language for mathematical text, mainly proofs by using a type theoretic approach. This is a subset of natural language.
  2. Semantics: We translate this controlled language to an abstract mathematical language (MathAbs). MathAbs is a system independent formal language for writing mathematics. We also solve some basic anaphora in this step.
In this demo, I will present the current status of MathNat development.
Vincent Laporte
Coq-GeoGebra interface
Abstract: This is a tool whose aim is to build and display a dynamic figure while a theorem of Euclidian geometry is proved. Based on Jean Duprat\'s formalization of this geometry in Coq, this tool is able to construct a figure from a proof context. Thanks to GeoGebra capabilities, the user is allowed to change the figure him or herself. Therefore this tool is also able to check a figure against the current context. Besides the figure evolves accordingly to the changes occurring in the proof context as the proof goes on. This interface has been designed so as to be extensible: it may easily take into account the modifications of the formalization. Moreover, its use might not be limited to this particular formalization of plane geometry.
Christophe Raffalli
Abstract: I shall present the current status of PML development. Notably, the termination test implemented by Pierre Hyvernat.

Social Events

  • The volunteers may have an easy mountain walk in the afternoon on the 14th
  • The dinner on the 14th will have some regional dishes.