An interactive assistant for the definition of proof certificates

Roberto Blanco 1 Zakaria Chihani 2
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
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.
Type de document :
Pré-publication, Document de travail
Preprint, presented at the Dale Fest seminar in honor of Professor Dale Miller's 60th birthday. 2016
Liste complète des métadonnées

https://hal.inria.fr/hal-01422829
Contributeur : Roberto Blanco <>
Soumis le : mardi 27 décembre 2016 - 12:10:49
Dernière modification le : mardi 17 avril 2018 - 09:08:55
Document(s) archivé(s) le : lundi 20 mars 2017 - 19:16:22

Fichier

blanco-chihani.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01422829, version 1

Collections

Citation

Roberto Blanco, Zakaria Chihani. An interactive assistant for the definition of proof certificates. Preprint, presented at the Dale Fest seminar in honor of Professor Dale Miller's 60th birthday. 2016. 〈hal-01422829〉

Partager

Métriques

Consultations de la notice

451

Téléchargements de fichiers

66