View: session overviewtalk overviewside by side with other conferences

09:00 | QED: a grand unified theory? SPEAKER: John Harrison |

09:35 | How to prove the odd order from the four color theorem SPEAKER: Georges Gonthier |

10:45 | 25 years of the Mizar Mathematical Library SPEAKER: Adam Grabowski ABSTRACT. Throughout the years, the development of the Mizar Mathematical Library was stimulated by large formalization projects, of which the proof of the Jordan Curve Theorem and the encoding of "Compendium of Continuous Lattices" were most influential. In Andrzej Trybulec's (the head of the Mizar project) opinion, expressed during QED II workshop in 1995, "one of the fundamental tasks of the QED effort should focus on reconstruction of the language and technology of mathematics." We will show how Andrzej's dreams of QED are implemented. |

11:20 | The seL4 microkernel verification SPEAKER: Gerwin Klein ABSTRACT. This talk will first give a brief high-level overview of the formal verification of the seL4 microkernel before showing some of its proof techniques in more detail. The aim will be to show examples of libraries and tactics for refinement, invariant, and security proofs for operating systems. |

11:55 | Towards Formally Verified Theorem Provers - Part I SPEAKER: Magnus Myreen |

12:15 | Towards Formally Verified Theorem Provers - Part II SPEAKER: Ramana Kumar |

12:30 | TBA SPEAKER: Claudio Sacerdoti Coen |

14:30 | TBA SPEAKER: Thomas C. Hales |

15:00 | Mixing proofs and computations SPEAKER: Michael Beeson ABSTRACT. In order to achieve the goals of QED, it will be necessary to effectively combine calculations and proofs in the same formal and computerized representation. We discuss the obstacles to this combination, and some of the attempts to overcome those obstacles. |

15:30 | The Naproche system: Proof-checking mathematical texts in controlled natural language SPEAKER: Marcos Cramer ABSTRACT. We have developed a controlled natural language (CNL) – i.e. a subset of a natural language defined through a formal grammar – for writing mathematical texts. The Naproche system can check the correctness of mathematical proofs written in this CNL. In this talk we will highlight some interesting logical and linguistic problems that had to be solved in the development of the Naproche CNL and the Naproche system: The system uses a formalism from the linguistic theory of presuppositions in order to work with potentially undefined terms, and can handle dynamic quantification, including the phenomenon of implicit dynamic function introduction, which had previously not been discussed in the literature. |

16:30 | QED and the TPTP World SPEAKER: Geoff Sutcliffe |

17:00 | MathHub.info: Active Mathematics SPEAKER: Michael Kohlhase ABSTRACT. We present the MathHub.info system, a development environment for active mathematical documents and an archive for flexiformal mathematics. It offers a rich interface for reading, writing, and interacting with mathematical documents and knowledge. The core MathHub.info system is an archive for flexiformal mathematical documents and libraries in the OMDoc/MMT format. Content can be authored or archived in the source format of the respective system, is versioned in GIT repositories, and transformed into OMDoc/MMT for machine-support and further into HTML5 for reading and interaction. |

17:30 | Hammering towards QED SPEAKER: Cezary Kaliszyk |