http://www.dagstuhl.de/16421

16. – 21. Oktober 2016, Dagstuhl Seminar 16421

Universality of Proofs

Organisatoren

Gilles Dowek (INRIA & ENS Cachan, FR)
Catherine Dubois (ENSIIE – Evry, FR)
Brigitte Pientka (McGill University – Montreal, CA)
Florian Rabe (Jacobs University Bremen, DE)


1 / 5 >

Auskunft zu diesem Dagstuhl Seminar erteilt

Dagstuhl Service Team

Dokumente

Teilnehmerliste
Gemeinsame Dokumente
Programm des Dagstuhl Seminars [pdf]

Motivation

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?

Classification

  • Semantics / Formal Methods
  • Verification / Logic

Keywords

  • Logics
  • Formal proofs
  • Provers
  • Reusability
  • Interoperability
  • Logical frameworks
  • Proof formats
  • Translation

Buchausstellung

Bücher der Teilnehmer 

Buchausstellung im Erdgeschoss der Bibliothek

(nur in der Veranstaltungswoche).

Dokumentation

In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.

 

Download Übersichtsflyer (PDF).

Publikationen

Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.