Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

An interactive assistant for the definition of proof certificates

Roberto Blanco 1 Zakaria Chihani 2
1 PARSIFAL - Proof search and reasoning with logic specifications
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
2 LRI - Laboratoire de Robotique Interactive
DIASI - Département Intelligence Ambiante et Systèmes Interactifs : DRT/LIST/DIASI
Abstract : The Foundational Proof Certificate (FPC) approach to proof evidence offers a flexible framework for the formal definition of proof semantics, described through its relationship to focused proof systems. The certificates thus produced by tools are executable when interpreted on top of a suitable logic engine, and can therefore be independently verified by trusted proof checkers. The fundamental obstacle encountered here lies in translating the proof evidence produced by a tool in the terms of a formal definition in the system. These formal definitions are akin to domain-specific languages (in which proofs can be written) programmed in the assembly language of the underlying proof systems: a delicate task for which both expert knowledge and great care are needed. To facilitate broader adoption, we begin to explore techniques that abstract away part of this complexity and bring the FPC framework closer to a user-friendly, programmable platform in which a wide range of high-level certificate definitions can be easily encoded.
Document type :
Preprints, Working Papers, ...
Complete list of metadatas
Contributor : Roberto Blanco <>
Submitted on : Tuesday, December 27, 2016 - 12:10:49 PM
Last modification on : Thursday, March 5, 2020 - 6:31:14 PM
Long-term archiving on: : Monday, March 20, 2017 - 7:16:22 PM


Files produced by the author(s)


  • HAL Id : hal-01422829, version 1



Roberto Blanco, Zakaria Chihani. An interactive assistant for the definition of proof certificates. 2016. ⟨hal-01422829⟩



Record views


Files downloads