MLPA on Thursday, July 15th

09:00‑10:00 Invited talk
Location: IF 1.16
09:00 Ulf Norell (Chalmers University)
Modules and records in Agda

In Agda, record types and modules are orthogonal features; record types are simple sigma types without any advanced features such as subtyping or row polymorphism, and modules are non-first class entities whose purpose is to manage names. I will show how modules and records play together to allow us to work with hierarchical structures without having to extend the language with more powerful features.

10:30‑12:30 Invited talks
Location: IF 1.16
10:30 Gerwin Klein (University of New South Wales)
Large-scale proof and libraries in Isabelle

In this presentation I will give an overview on the experience on proof-reuse and proof-libraries in Isabelle/HOL in two areas. The first is the L4.verified project, a large-scale proof of implementation correctness on the C level of the seL4 Operating Systems Microkernel. The proof consists of 200,000 lines of Isabelle script, includes multiple frameworks and libraries, had used external developments in core areas, and has contributed libraries and components back into the Isabelle distribution. The second part of the talk will be about the experience so far in submissions and re-use in the Archive of Formal Proofs (AFP), an archive of user-contributed Isabelle developments and libraries.

11:30 Andrzej Trybulec (University of Bialystok)
Mizar Mathematical Library - a large repository of formalized mathematics

Mizar is a computer system verifying mathematical proofs translated to or written in the Mizar language. The Mizar Mathematical Library (MML) is the main repository of formalized and computer-checked mathematics. Over two hundred authors contributed to the MML, which at the present includes almost ten thousand definitions and over fifty thousand theorems with complete proofs. The Hahn-Banach theorem, the Bing and Nagata-Smirnow metrization theorems, the Jordan curve theorem, and the Brouwer fixed point theorem are among the most advanced theorems contributed. The goal of the talk is to describe semantic mechnisms: structures, attributes and registrations used to develop abstract mathematics in Mizar.

14:00‑15:00 Invited talk
Location: IF 1.16
14:00 Don Sannella (University of Edinburgh)
Proofs in structured specifications

Work on structured algebraic specifications provide syntax and semantics for a module language for proof assistants, together with a rich theory giving useful connections to relevant notions including module refinement and transformation. Modules can be built using different logical systems, once appropriate connections between the logics in use are provided. This theory takes a mainly model-oriented point of view, and proofs turn out to be less straightforward than one might wish. I will give an overview of this body of work, with stress on the issues that arise in connection with proof.

15:30‑17:30 Invited talks
Location: IF 1.16
15:30 Dale Miller (INRIA)
Towards a broad spectrum proof certificate

Proof assistants and automated theorem provers generally produce evidence of a successful proof in an assortment of (often ad hoc) formats. The extent to which one prover can understand and check such evidence from another prover is the extent to which they can successfully inter-operate. I will outline some recent work on providing a single proof system that can be tuned so that it can host proof systems such as sequent calculus, natural deduction, tableau, and tabled deduction for classical and intuitionistic logics. A proof checker for the hosting proof system can then immediately be a proof checker for all of these other proof systems. The hope is that such a flexible format for proof certificates can be the basis of a lingua franca among proof systems. Central to this work is the use of linear logic and focused proof systems.

16:30 Adam Chlipala (Harvard University)
A Bottom-Up Approach to Safe Low-Level Programming

It's hard to please everyone with a systems programming language. If we follow the usual rules of language design, every programmer will miss some feature and complain that some feature should have been left out. Safe programming languages rely on increasingly complicated (and often arbitrary-seeming) type systems and program analyses, and yet still these features don't support full verification. What if we stopped trying to design a single language and instead let programmers implement language features as libraries? With traditional compiler architectures, it would be very hard to ensure that the different features played well together... but what if our platform is a proof assistant, not a traditional compiler? In this talk, I will discuss some preliminary experiments of that kind: implementing an open "systems language" via Coq metaprogramming libraries that build verified machine code programs.