From May 5 to May 9, at Institut Henri Poincaré. May 8 will be off as it is holliday in France.
We expect the talks at the workshop in the following three areas:
|Monday 5 May|
|11h00-12h00||John Harrison||Formal proof: current progress and outstanding challenges|
|14h00-15h00||Enrico Tassi||Mathematical Components, a large library of formalized mathematics|
|15h15-16h15||Artur Kornilowicz||Structures and structural types in Mizar|
|16h45-17h45||Tobias Nipkow||Tame graph enumeration in Flyspeck|
|Tuesday 6 May|
Christopher A. Stone
|Brazilian type checking|
|11h00-12h00||Guillaume Brunerie||Cubical Homotopy Type Theory|
|14h00-15h00||Benedikt Ahrens||Formalizing category theory in type theory|
|15h15-16h15||Karol Pak||Formalization of n-dimensional manifolds in Mizar|
|16h45-17h45||Dan Licata||Eilenberg-MacLane spaces in Homotopy Type Theory|
|Wednesday 7 May|
|9h30-10h30||Thomas Hales||Solovyev's formal computations in HOL Light|
|11h00-12h00||Daniel Grayson||Formalization of elementary algebraic K-theory in Coq with Univalent Foundations|
|14h00-15h00||Peter LeFanu Lumsdaine||Recent coherence theorems for dependent type theory|
|16h45-17h45||Urs Schreiber||Classical field theory and Quantization via Cohesive and Linear homotopy types|
|18h30-21h00||Reception in Jussieu tower|
|Friday 9 May|
|9h30-10h30||Freek Wiedijk||Formal proof done right|
|11h00-12h00||Norman Megill||The Metamath proof language|
|14h00-15h00||Bill Richter||Hilbert axiomatic geometry and readable HOL Light proofs|
|15h15-16h15||Josef Urban||Inductive and deductive AI over large formal libraries|
|16h45-17h45||Ursula Martin||How do formal proofs happen?|
Formalizing category theory in type theory
Andrej Bauer (University of Ljubljana, Slovenia), Christopher A. Stone (Harvey Mudd College, USA)
Brazilian type checking
Proof assistants verify that inputs are correct up to judgmental equality. Proofs are easier and smaller if equalities without computational content are verified by an oracle, because proof terms for these equations can be omitted. In order to keep judgmental equality decidable, though, typical proof assistants use a limited definition implemented by a fixed equivalence algorithm. While other equalities can be expressed using propositional identity types and explicit equality proofs and coercions, in some situations these create prohibitive levels of overhead in the proof.
Voevodsky has proposed a type theory with two identity types, one propositional and one judgmental. This lets us hypothesize new judgmental equalities for use during type checking, but generally renders the equational theory undecidable without help from the user.
Rather than reimpose the full overhead of term-level coercions for judgmental equality, we propose algebraic effect handlers as a general mechanism to provide local extensions to the proof assistant's algorithms. As a special case, we retain a simple form of handlers even in the final proof terms, small proof-specific hints that extend the trusted verifier in sound ways.
Cubical Homotopy Type Theory
Daniel Grayson (Urbana/IAS)
Formalization of elementary algebraic K-theory in Coq with Univalent Foundations
Structures and structural types in Mizar
Formal proof: current progress and outstanding challenges
Solovyev's formal computations in HOL Light
Peter LeFanu Lumsdaine
Recent coherence theorems for dependent type theory
Mathematicians' confidence in dependent type theory as a system for developing mathematics is based, in large part, on its models in traditional mathematical settings. The general theory of such models was set down in the 80's and 90's in the work of Cartmell and others (contextual categories, categories with attributes, … ), satisfactorily in most respects but with one major problem outstanding: the so-called coherence problem, of how to deal with the fact that mathematical structures are typically characterised only up to isomorphism, while models of syntax must be well-behaved up to on-the-nose equality.
After a gap of some years, several advances on this problem have recently appeared (variously by Voevodsky, Curien–Garner–Hofmann, and Lumsdaine–Warren). I will survey the connections between these and earlier results, and their limitations, and discuss the obstacles to proving an “ultimate coherence theorem”.
Eilenberg-MacLane spaces in Homotopy Type Theory
The Metamath proof language
Tame graph enumeration in Flyspeck
Formalization of n-dimensional manifolds in Mizar
Hilbert axiomatic geometry and readable HOL Light proofs
Classical field theory and Quantization via Cohesive and Linear homotopy types
We discuss how (at least considerable parts of) modern fundamental physics in the guise of local Lagrangian quantum gauge field theory may be naturally and usefully formalized in a cohesive and linear version of homotopy type theory. Our discussion takes place in infinity-categorical semantics but is phrased such as to lend itself to a fully syntactic formulation. Background material for the talk is available at
We will discuss some informal observations about the relationship between reasoning happening in the interior and on the exterior of a system.
Inductive and deductive AI over large formal libraries
Mathematical Components, a large library of formalized mathematics
Formal proof done right
What is currently the best system for formal proof?
And what is most sorely missing there?
The list of participants can be found on IHP's website.