Towards typed repositories of proofsReportar como inadecuado

Towards typed repositories of proofs - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

* Corresponding author 1 DISI - Department of Computer Science and Engineering Bologna 2 PPS - Preuves, Programmes et Systèmes 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.

Keywords : version control system programming language proof assistant incremental type-checking type theory

Autor: Matthias Puech - Yann Regis-Gianas -



Documentos relacionados