Modules and Libraries for Proof Assistants (MLPA-10)
15 July 2010, Edinburgh
affiliated with IJCAR and ITP as part of FLoC
Description
This was the second workshop on module systems and libraries for proof assistants succeeding MLPA-09, which was held during CADE-22. It was held at FLoC.
The program consisted only of invited talks:
- Adam Chlipala: A Bottom-Up Approach to Safe Low-Level Programming
slides
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.
- Gerwin Klein: Large-scale proof and libraries in Isabelle
slides
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.
- Dale Miller: Towards a broad spectrum proof certificate
slides
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.
- Ulf Norell: Modules and records in Agda
slides
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.
- Don Sannella: Proofs in structured specifications
slides
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.
- Andrzej Trybulec: 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.
Collection of abstracts in pdf format.
Goals
Over the last twenty years, users of proof assistants and automated theorem provers have created large libraries of formal proofs and mathematical knowledge.
Module systems help with the tedious tasks of organizing, sharing, and maintaining libraries. In the view of the ever increasing complexity of this network of information, module systems offer many of the answers to the practical problems that proof assistant system developers face today and can therefore be seen as an emerging research for the automated deduction community.
The workshop aims to attract and bring together researchers and practitioners with background and experience in the design, implementation, and application of module systems from different logic-based systems such as theorem provers, proof assistants, and programming languages.
Because it is affiliated with both and takes place between ITP and IJCAR, the workshop will provide the fertile venue for the exchange of ideas and experiences and has the potential to impact the way we organize proofs and programs in the future.
Organization
Program Committee
- Stefan Berghofer, Institut für Informatik, Technische Universität München
- Derek Dreyer, Max Planck Institute for Software Systems, Saarbrücken
- Georges Gonthier, Microsoft Research, Cambridge
- Zhaohui Luo, Royal Holloway, University of London,
- Till Mossakowski, German research center for artificial intelligence, Bremen,
- Scott Owens, Computer Laboratory, University of Cambridge
- Florian Rabe, Jacobs University Bremen (chair)
- Carsten Schürmann, IT University of Copenhagen (chair)