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.
Document type :
Conference papers
Complete list of metadatas

Contributor : Matthieu Sozeau <>
Submitted on : Monday, May 21, 2012 - 11:49:09 AM
Last modification on : Friday, January 4, 2019 - 5:33:25 PM


  • HAL Id : hal-00699581, version 1



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



Record views