Towards typed repositories of proofs

Matthias Puech 1 Yann Régis-Gianas 2, 3, *
* Auteur correspondant
3 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 : In this paper, we advocate for an architecture for proof assistants and programming language tools that is closer to the daily workflow of their users. Indeed, most of the mathematician or programmer's time is spent editing, not writing. As a consequence, the usual interaction loop "(edit; compile)*; commit" is an over-approximation that does not scale when compilation is replaced by proof-checking. We propose an enhancement and an adaptation of version control paradigms to the management of proof repositories, to witness with more precision the impact of changes. We sketch a dependently typed language that would be a kernel language to build such a framework upon.
Type de document :
Communication dans un congrès
Mathematically Intelligent Proof Search - MIPS 2010, Jul 2010, Paris, France. 2010
Liste complète des métadonnées

Littérature citée [12 références]  Voir  Masquer  Télécharger
Contributeur : Yann Regis-Gianas <>
Soumis le : mercredi 13 octobre 2010 - 08:52:51
Dernière modification le : jeudi 11 janvier 2018 - 06:22:37
Document(s) archivé(s) le : jeudi 25 octobre 2012 - 17:10:32


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00525874, version 1




Matthias Puech, Yann Régis-Gianas. Towards typed repositories of proofs. Mathematically Intelligent Proof Search - MIPS 2010, Jul 2010, Paris, France. 2010. 〈inria-00525874〉



Consultations de la notice


Téléchargements de fichiers