Universality of Proofs
( 16. Oct – 21. Oct, 2016 )
- Gilles Dowek (INRIA & ENS Cachan, FR)
- Catherine Dubois (ENSIIE - Evry, FR)
- Brigitte Pientka (McGill University - Montreal, CA)
- Florian Rabe (Jacobs University Bremen, DE)
- Annette Beyer (für administrative Fragen)
Proof systems are programs that allow a user to build formal proofs either interactively or automatically. Building such a formal proof is always difficult - for instance the Feit-Thompson odd order theorem, the CompCert verified C compiler, the seL4 verified operating system micro-kernel and the proof of the Kepler conjecture, required several years of medium to large teams to be completed. Thus, the fact that these proofs are specific to one logic, sometimes to one proof system or even to one specific version of a system, is a severe limitation to the diffusion of proof systems among mathematicians and computer scientists. Comparing to software engineering, we are still very far from having "off-the-shelf" components, "proving in the large" techniques and "interoperability" of theories. However some partial answers exist: point to point translations, proof standards and logical frameworks have been developed by researchers in different communities. This also relies on techniques that adapt and package together existing formalizations. While some answers exists (e.g. modules, traits, features, and inheritance), there is no overarching, general foundation and methodology.
This Dagstuhl Seminar aims to bring together the different communities and to build a stronger community around these issues.
The synergy between researchers coming from different fields of computer science (logic, proof engineering, program verification, formal mathematics) will be essential to learn about and reconcile the different approaches. In particular, this will allow us to develop a common objective and framework for proof developments that support the communication, reuse and interoperability of proofs. More precisely, the research questions pursued include:
- Why are current systems not more interoperable? What design changes are necessary to increase interoperability in the future?
- What are the current approaches towards interoperability? How successful or promising are they?
- How can correctness be guaranteed in a distributed setting? Should there be a single universal checker (which would be hard to agree on) or many decentral ones (which may preclude interoperability)?
- How can we design interchange languages that naturally subsume existing (and future!) formal systems?
- Should a logical framework permit the definition of any logical system? Or do the logics currently implemented have points in common that could be hard wired into the framework itself?
- How reasonable is it to propose a single universal proof format? Or do we need different formats for different families of proof systems and a partial interoperability between the formats? How should a proof format be evaluated (generality, conciseness, efficiency of proof checking, ...)?
- How should universal proof library be exchanged? Is Web technology sufficient or do we need specific tools to organize data bases of proofs?
- How can we practically and reliably relate individual systems with their representation in an interchange format or a logical framework? How can two systems agree on the meaning of an exchanged theorem and thus trust each other?
Proof systems are software systems that allow us to build formal proofs, either interactively or automatically, and to check the correctness of such proofs. Building such a formal proof is always a difficult task -- for instance the Feit-Thompson odd order theorem, the CompCert verified C compiler, the seL4 verified operating system micro-kernel, and the proof of the Kepler conjecture required several years with a medium to large team of developers to be completed. Moreover, the fact that each of these proofs is formalized in a specific logic and the language of a specific proof tool is a severe limitation to its dissemination within the community of mathematicians and computer scientists. Compared to many other branches of computer science, for instance software engineering, we are still very far from having off-the-shelf and ready-to-use components, "proving in the large" techniques, and interoperability of theory and systems. However, several teams around the world are working on this issue and partial solutions have been proposed including point-to-point translations, proof standards, and logical frameworks. Yet, a lot still remains to be done as there is currently no overarching general foundation and methodology.
This seminar has been organized to bring together researchers from different communities, such as automated proving, interactive proving and SAT/SMT solving as well as from logic, proof engineering, program verification and formal mathematics. An essential goal has been to form a community around these issues in order to learn about and reconcile these different approaches. This will allow us to develop a common objective and framework for proof developments that support the communication, reuse, and interoperability of proofs.
The program of the seminar included introductions to different methods and techniques, the definition of precise objectives, and the description of recent achievements and current trends. It consisted of 30 contributed talks from experts on the above topics and six breakout sessions on major problems: theory graph -- based reasoning, benchmarks, conflicting logics and system designs, proof certificates, design of a universal library of elementary mathematics, and a standard for system integration and proof interchange. The contributed talks took place in the morning, and two parallel breakout sessions each took place on Monday, Tuesday and Thursday afternoon, followed by plenary discussions organized by each session's moderator.
The organizers would like to thank the Dagstuhl team and all the participants for making this first seminar a success and, hopefully, an event to be repeated.
- Andreas Martin Abel (Chalmers UT - Göteborg, SE) [dblp]
- Jesús María Aransay Azofra (University of La Rioja - Logroño, ES) [dblp]
- Christoph Benzmüller (FU Berlin, DE) [dblp]
- Jasmin Christian Blanchette (MPI für Informatik - Saarbrücken, DE) [dblp]
- Frédéric Blanqui (ENS - Cachan, FR) [dblp]
- Peter Brottveit Bock (IT University of Copenhagen, DK) [dblp]
- Venanzio Capretta (University of Nottingham, GB) [dblp]
- Benjamin Delaware (Purdue University - West Lafayette, US) [dblp]
- Gilles Dowek (INRIA & ENS Cachan, FR) [dblp]
- Catherine Dubois (ENSIIE - Evry, FR) [dblp]
- William M. Farmer (McMaster University - Hamilton, CA) [dblp]
- Amy Felty (University of Ottawa, CA) [dblp]
- Thibault Gauthier (Universität Innsbruck, AT) [dblp]
- Frédéric Gilbert (ENS - Cachan, FR) [dblp]
- Georges Gonthier (INRIA Saclay - Île-de-France, FR) [dblp]
- Stéphane Graham-Lengrand (Ecole Polytechnique - Palaiseau, FR) [dblp]
- Hugo Herbelin (University Paris-Diderot, FR) [dblp]
- Olivier Hermant (Ecole des Mines de Paris, FR) [dblp]
- Guy Katz (Stanford University, US) [dblp]
- Chantal Keller (University of Paris Sud - Orsay, FR) [dblp]
- Michael Kohlhase (Universität Erlangen-Nürnberg, DE) [dblp]
- Ramana Kumar (Data61 / NICTA - Sydney, AU) [dblp]
- Dale Miller (INRIA Saclay - Île-de-France, FR) [dblp]
- Alberto Momigliano (University of Milan, IT) [dblp]
- César A. Muñoz (NASA Langley - Hampton, US) [dblp]
- Adam Naumowicz (University of Bialystok, PL) [dblp]
- Brigitte Pientka (McGill University - Montreal, CA) [dblp]
- Elaine Pimentel (Federal University of Rio Grande do Norte, BR) [dblp]
- Florian Rabe (Jacobs University Bremen, DE) [dblp]
- Claudio Sacerdoti Coen (University of Bologna, IT) [dblp]
- Ivan Scagnetto (University of Udine, IT) [dblp]
- Gert Smolka (Universität des Saarlandes, DE) [dblp]
- René Thiemann (Universität Innsbruck, AT) [dblp]
- Josef Urban (Czech Technical University - Prague, CZ) [dblp]
- Laurent Voisin (SYSTEREL Aix-en-Provence, FR) [dblp]
- Freek Wiedijk (Radboud University Nijmegen, NL) [dblp]
- Bruno Woltzenlogel Paleo (Australian National University - Canberra, AU) [dblp]
- semantics / formal methods
- verification / logic
- formal proofs
- logical frameworks
- proof formats