Lightweight proof by reflection using a posteriori simulation of effectful computation

Guillaume Claret 1, 2 Lourdes del Carmen Gonzalez Huesca 1, 2 Yann Régis-Gianas 2 Beta Ziliani 3
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Abstract : Proof-by-reflection is a well-established technique that em- ploys decision procedures to reduce the size of proof-terms. Currently, decision procedures can be written either in Type Theory--in a purely functional way that also ensures termination-- or in an effectful program- ming language, where they are used as oracles for the certified checker. The first option offers strong correctness guarantees, while the second one permits more efficient implementations. We propose a novel technique for proof-by-reflection that marries, in Type Theory, an effectful language with (partial) proofs of correctness. The key to our approach is to use simulable monads, where a monad is simulable if, for all terminating reduction sequences in its equivalent effectful computational model, there exists a witness from which the same reduction may be simulated a posteriori by the monad. We encode several examples using simulable monads and demonstrate the advantages of the technique over previous approaches.
Type de document :
Communication dans un congrès
Interactive Theorem Proving, Jul 2013, Rennes, France. 2013
Liste complète des métadonnées

Littérature citée [15 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00870110
Contributeur : Yann Regis-Gianas <>
Soumis le : samedi 5 octobre 2013 - 10:04:35
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : vendredi 7 avril 2017 - 06:55:21

Fichier

simulation-based-pbr-final.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00870110, version 1

Collections

INRIA | PPS | USPC

Citation

Guillaume Claret, Lourdes del Carmen Gonzalez Huesca, Yann Régis-Gianas, Beta Ziliani. Lightweight proof by reflection using a posteriori simulation of effectful computation. Interactive Theorem Proving, Jul 2013, Rennes, France. 2013. 〈hal-00870110〉

Partager

Métriques

Consultations de la notice

640

Téléchargements de fichiers

228