Registration
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 | ||
---|---|---|
10h00-10h45 | Registration | |
10h45-11h00 | Georges Gonthier, Vladimir Voevodsky | Introduction |
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 | ||
9h30-10h30 | Andrej Bauer, 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 |
15h15-16h15 | Carlos Simpson | Interior/Exterior |
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? |
Benedikt Ahrens
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.
Guillaume Brunerie
Cubical Homotopy Type Theory
Daniel Grayson (Urbana/IAS)
Formalization of elementary algebraic K-theory in Coq with Univalent Foundations
Artur Kornilowicz
Structures and structural types in Mizar
John Harrison
Formal proof: current progress and outstanding challenges
Thomas Hales
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”.
Dan Licata
Eilenberg-MacLane spaces in Homotopy Type Theory
Norman Megill
The Metamath proof language
Tobias Nipkow
Tame graph enumeration in Flyspeck
Karol Pak
Formalization of n-dimensional manifolds in Mizar
Bill Richter
Hilbert axiomatic geometry and readable HOL Light proofs
Urs Schreiber
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
http://ncatlab.org/schreiber/show/Classical+field+theory+via+Cohesive+homotopy+types http://ncatlab.org/schreiber/show/Quantization+via+Linear+homotopy+types
Carlos Simpson
Interior/Exterior
We will discuss some informal observations about the relationship between reasoning happening in the interior and on the exterior of a system.
Josef Urban
Inductive and deductive AI over large formal libraries
Enrico Tassi
Mathematical Components, a large library of formalized mathematics
Freek Wiedijk
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.