License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagRep.6.10.75
URN: urn:nbn:de:0030-drops-69514
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/6951/
Go back to Dagstuhl Reports

Dowek, Gilles ; Dubois, Catherine ; Pientka, Brigitte ; Rabe, Florian
Weitere Beteiligte (Hrsg. etc.): Gilles Dowek and Catherine Dubois and Brigitte Pientka and Florian Rabe

Universality of Proofs (Dagstuhl Seminar 16421)

pdf-format:
dagrep_v006_i010_p075_s16421.pdf (1.0 MB)

Abstract

This report documents the program and the outcomes of Dagstuhl Seminar 16421 "Universality of Proofs" which took place October 16-21, 2016.

The seminar was motivated by the fact that it is nowadays difficult to exchange proofs from one proof assistant to another one. Thus a formal proof cannot be considered as a universal proof, reusable in different contexts. The seminar aims at providing a comprehensive overview of the existing techniques for interoperability and going further into the development of a common objective and framework for proof developments that support the communication, reuse and interoperability of proofs.

The seminar included participants coming from different fields of computer science such as logic, proof engineering, program verification, formal mathematics. It included overview talks, technical talks and breakout sessions. This report collects the abstracts of talks and summarizes the outcomes of the breakout sessions.

BibTeX - Entry

@Article{dowek_et_al:DR:2017:6951,
  author =	{Gilles Dowek and Catherine Dubois and Brigitte Pientka and Florian Rabe},
  title =	{{Universality of Proofs (Dagstuhl Seminar 16421)}},
  pages =	{75--98},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2017},
  volume =	{6},
  number =	{10},
  editor =	{Gilles Dowek and Catherine Dubois and Brigitte Pientka and Florian Rabe},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/6951},
  URN =		{urn:nbn:de:0030-drops-69514},
  doi =		{10.4230/DagRep.6.10.75},
  annote =	{Keywords: Formal proofs, Interoperability, Logical frameworks, Logics, Proof formats, Provers, Reusability}
}

Keywords: Formal proofs, Interoperability, Logical frameworks, Logics, Proof formats, Provers, Reusability
Collection: Dagstuhl Reports, Volume 6, Issue 10
Issue Date: 2017
Date of publication: 01.03.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI