Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.

Formalization of mathematics in proof assistants

Dates and location

From May 5 to May 9, at Institut Henri Poincaré. May 8 will be off as it is holliday in France.

Description

We expect the talks at the workshop in the following three areas:

  1. About successful formalizations of various areas, results and methods of mathematics in proof assistants.
  2. About new tools for proof assistants developed in order to facilitate formalization of mathematics.
  3. About the limitations of current proof assistants which prevent efficient formalization of various mathematical ideas and about possible suggestions on how to overcome these limitations.

Planning

Monday 5 May
10h00-10h45Registration
10h45-11h00Georges Gonthier,
Vladimir Voevodsky
Introduction
11h00-12h00John HarrisonFormal proof: current progress and outstanding challenges
14h00-15h00Enrico TassiMathematical Components, a large library of formalized mathematics
15h15-16h15Artur KornilowiczStructures and structural types in Mizar
16h45-17h45Tobias NipkowTame graph enumeration in Flyspeck
Tuesday 6 May
9h30-10h30Andrej Bauer,
Christopher A. Stone
Brazilian type checking
11h00-12h00Guillaume BrunerieCubical Homotopy Type Theory
14h00-15h00Benedikt AhrensFormalizing category theory in type theory
15h15-16h15Karol PakFormalization of n-dimensional manifolds in Mizar
16h45-17h45Dan LicataEilenberg-MacLane spaces in Homotopy Type Theory
Wednesday 7 May
9h30-10h30Thomas HalesSolovyev's formal computations in HOL Light
11h00-12h00Daniel GraysonFormalization of elementary algebraic K-theory in Coq with Univalent Foundations
14h00-15h00Peter LeFanu LumsdaineRecent coherence theorems for dependent type theory
15h15-16h15Carlos SimpsonInterior/Exterior
16h45-17h45Urs SchreiberClassical field theory and Quantization via Cohesive and Linear homotopy types
18h30-21h00Reception in Jussieu tower
Friday 9 May
9h30-10h30Freek WiedijkFormal proof done right
11h00-12h00Norman MegillThe Metamath proof language
14h00-15h00Bill RichterHilbert axiomatic geometry and readable HOL Light proofs
15h15-16h15Josef UrbanInductive and deductive AI over large formal libraries
16h45-17h45Ursula MartinHow do formal proofs happen?

Talks

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?

Participants

The list of participants can be found on IHP's website.

Organizers

workshop_1.txt · Last modified: 2014/05/07 08:04 by smimram
Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.
www.chimeric.de Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0