Skip to Main content Skip to Navigation
Conference papers

A Distributed and Trusted Web of Formal Proofs

Dale Miller 1
1 PARTOUT - Automatisation et ReprésenTation: fOndation du calcUl et de la déducTion
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : Most computer checked proofs are tied to the particular technology of a prover's software. While sharing results between proof assistants is a recognized and desirable goal, the current organization of theorem proving tools makes such sharing an exception instead of the rule. In this talk, I argue that we need to turn the current architecture of proof assistants and formal proofs inside-out. That is, instead of having a few mature theorem provers include within them their formally checked theorems and proofs, I propose that proof assistants should sit on the edge of a web of formal proofs and that proof assistant should be exporting their proofs so that they can exist independently of any theorem prover. While it is necessary to maintain the dependencies between definitions, theories, and theorems, no explicit library structure should be imposed on this web of formal proofs. Thus a theorem and its proofs should not necessarily be located at a particular URL or within a particular prover's library. While the world of symbolic logic and proof theory certainly allows for proofs to be seen as global and permanent objects, there is a lot of research and engineering work that is needed to make this possible. I describe some of the required research and development that must be done to achieve this goal.
Document type :
Conference papers
Complete list of metadata

Cited literature [50 references]  Display  Hide  Download

https://hal.inria.fr/hal-02468229
Contributor : Dale Miller <>
Submitted on : Wednesday, February 5, 2020 - 3:56:43 PM
Last modification on : Friday, April 30, 2021 - 10:02:10 AM
Long-term archiving on: : Wednesday, May 6, 2020 - 6:09:08 PM

File

icdcit-2020.pdf
Files produced by the author(s)

Identifiers

Citation

Dale Miller. A Distributed and Trusted Web of Formal Proofs. ICDCIT 2020 - 16th International Conference on Distributed Computing and Internet Technology, Jan 2020, Bhubaneswar, India. pp.21-40, ⟨10.1007/978-3-030-36987-3_2⟩. ⟨hal-02468229⟩

Share

Metrics

Record views

201

Files downloads

515