QED+20, FRIDAY, JULY 18TH 2014

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.

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.

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.

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.

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.