# 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
*Id _{A}(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*

- 19:00 —
- May the 12th
- 09:00 —
*Registration* - 12:30 —
*Lunch* - 14:00 — Bruno Barras — abstract — slides
*Extending the Implicit Calculus of Constructions with Union and Subset Types*- 14:30 — Chantal Keller — abstract — slides
*Importing HOL-Light into Coq : deep and shallow embeddings of the higher order logic into Coq*- 15:00 — Lionel Vaux — abstract — slides
*Primitive recursion in finiteness spaces*- 15:30 —
*Coffee Break* - 16:00 — Cody Roux — abstract — slides
*Normalisation by set theoretic models and labelling*- 16:30 — Neil Sculthorpe — abstract — slides
*Safe Functional Reactive Programming through Dependent Types*- 17:00 — Denis Cousineau — abstract — slides
*How to prove strong normalization from weak normalization, the case of minimal deduction modulo*- 17:45 —
*Demo session* - 19:00 —
*Dinner*

- 09:00 —
- May the 13th
- 09:00 — Pawel Urzyczyn (invited) — abstract — slides
*Decision problems in polymorphic type assignment*- 10:00 — Johannes Kanig — abstract — slides
*Proof of Higher-Order Programs using Effect Polymorphism*- 10:30 —
*Coffee Break* - 11:00 — Jean Duprat — abstract — slides
*Plane geometry for pupils in Coq*- 11:30 — Enrico Tassi — abstract — slides
*Hints in unification*- 12:00 — Claudio Sacerdoti Coen — abstract — slides
*Matita NG: reduction and type-checking*- 12:30 —
*Lunch* - 14:00 — Andreas Abel — abstract — slides
*Normalization by Evaluation for Impredicative Type Theory (Work in Progress)*- 14:30 — Paola Toto — abstract — slides
*Algebraic setting for many-valued constructive topology*- 15:00 — Ugo de Liguoro — abstract — slides
*An interactive concept of integer and boolean to model classical arithmetic constructively*- 15:30 —
*Coffee Break* - 16:00 — Randy Pollack — abstract — slides
*A new canonical representation of binding*- 16:30 — Tom Hirschowitz — abstract — slides
*Contraction-free proofs and games for Linear Logic*- 17:00 — Matthieu Sozeau — slides
*A New Look at Generalized Rewriting in Type Theory*

Abstract: Rewriting is an essential tool for computer-based reasoning, both automated and assisted. In a proof assistant, rewriting can be used to replace terms in arbitrary contexts, generalizing the usual equational reasoning to reasoning modulo arbitrary relations. This can be done provided the necessary proofs that functions appearing in goals are congruent with respect to specific relations. We present a new implementation of generalized rewriting in the Coq proof assistant, making essential use of the expressive power of dependent types and a recently implemented type class mechanism. The tactic improves on and generalizes previous versions by supporting natively higher-order functions (rewriting under binders), polymorphism and subrelations. We demonstrate how the type class system inspired from Haskell can provide a natural interface between the user and such tactics, making them easily extensible.- 17:45 —
*Demo session* - 19:00 —
*Dinner*

- May the 14th
- 09:00 — Peter Hancock (invited) — abstract — slides
*Entering bars infinitely often*- 10:00 — Ioana Pasca — abstract — slides
*Formal verification of exact computations using Newton\'s method*- 10:30 —
*Coffee Break* - 11:00 — Thorsten Altenkirch — abstract — slides
*PiSigma a core language for dependently typed programming*- 11:30 — Hugo Herbelin — abstract — slides
*Investigations into Kripke models for classical logic*- 12:00 — Michael Lienhardt — abstract — slides
*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) — abstract — slides
*Topological and higher-dimensional aspects of type theory*- 10:00 — Zhaohui Luo — abstract — slides
*Dependent Record Types Revisited*- 10:30 —
*Coffee Break* - 11:00 — Nils Anders Danielsson — abstract — slides
*Mixing Induction and Coinduction*- 11:30 — Clement Houtmann — abstract — slides
*Cut-elimination Canonicity for Classical Sequent Calculus*- 12:00 — Dulma Rodriguez — abstract — slides
*Efficient Type-Checking for Amortised Heap-Space Analysis*- 12:30 —
*Lunch* - 14:00 — Damien Pous — abstract — slides
*Typing and Untyping Various Algebras*- 14:30 — Francois Garillot — abstract — slides
*Working effectively with generic subgroups*- 15:00 —
*Coffee Break* - 15:30 — Micaela Mayero — abstract — slides
*Certification of Numerical Analysis Programs*- 16:00 — Barbara Petit — abstract — slides
*A lambda calculus with pattern matching and polymorphims*

## Demos

- 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:*Syntax:*We develop a controlled language for mathematical text, mainly proofs by using a type theoretic approach. This is a subset of natural language.*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.

- 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
*PML*

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.