An interactive assistant for the definition of proof certificates - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2016

An interactive assistant for the definition of proof certificates

Résumé

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.
Fichier principal
Vignette du fichier
blanco-chihani.pdf (319.98 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-01422829 , version 1 (27-12-2016)

Identifiants

  • HAL Id : hal-01422829 , version 1

Citer

Roberto Blanco, Zakaria Chihani. An interactive assistant for the definition of proof certificates. 2016. ⟨hal-01422829⟩
355 Consultations
81 Téléchargements

Partager

Gmail Facebook X LinkedIn More