Elaborations in Type Theory

Matthieu Sozeau 1
1 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 : Dependent Type Theory as implemented into proof assistants and programming languages like Coq and Agda provide a firm and general basis for the formalization of mathematics and computer software. However, the core dependent type theory exposes a rather spartan interface for programming and writing proofs. Over the years a number of higher-level constructs and techniques have been developed to overcome this difficulty without touching the core language. For instance, implicit syntax, tactics and meta-languages like Ltac have been used successfully to make systems more accessible, automatable and scalable. Our research investigates further elaborations from high-level languages into dependent type theory. We present three such elaborations that facilitate programming with proofs, inductive families and overloaded functions in the Coq proof assistant. We demonstrate their usefulness for defining objects and structuring developments, as well as their crucial help in proofs.
Type de document :
Communication dans un congrès
DTP'10 - Dependently Typed Programming - 2010, Jul 2010, Edinburgh, United Kingdom. 2010
Liste complète des métadonnées

Contributeur : Matthieu Sozeau <>
Soumis le : lundi 21 mai 2012 - 11:49:09
Dernière modification le : jeudi 15 novembre 2018 - 20:27:28


  • HAL Id : hal-00699581, version 1



Matthieu Sozeau. Elaborations in Type Theory. DTP'10 - Dependently Typed Programming - 2010, Jul 2010, Edinburgh, United Kingdom. 2010. 〈hal-00699581〉



Consultations de la notice