Elaboration in Dependent Type Theory

Reference. Elaboration in Dependent Type Theory

Leonardo de Moura, Jeremy Avigad, Soonho Kong, Cody Roux · arXiv · 2015 · type-theory · arXiv

To be usable in practice, interactive theorem provers need to provide convenient and efficient means of writing expressions, definitions, and proofs. This involves inferring information that is often left implicit in an ordinary mathematical text, and resolving ambiguities in mathematical expressions. We refer to the process of passing from a quasi-formal and partially-specified expression to a completely precise formal one as elaboration. We describe an elaboration algorithm for dependent type theory that has been implemented in the Lean theorem prover. Lean’s elaborator supports higher-order unification, type class inference, ad hoc overloading, insertion of coercions, the use of tactics, and the computational reduction of terms. The interactions between these components are subtle and complex, and the elaboration algorithm has been carefully designed to balance efficiency and usability. We describe the central design goals, and the means by which they are achieved.

Cite

Cite as @moura-2015-elaboration (helia, typst) · \cite{moura-2015-elaboration} (LaTeX)

BibTeX

bibtex · 8 lines

@misc{moura-2015-elaboration,
  author = {Leonardo de Moura and Jeremy Avigad and Soonho Kong and Cody Roux},
  title = {Elaboration in Dependent Type Theory},
  year = {2015},
  month = {5},
  eprint = {1505.04324},
  archiveprefix = {arXiv}
}

hayagriva YAML (typst)

yaml · 13 lines

moura-2015-elaboration:
  type: misc
  title: Elaboration in Dependent Type Theory
  author:
  - name: Moura
    given-name: Leonardo
    prefix: de
  - Avigad, Jeremy
  - Kong, Soonho
  - Roux, Cody
  date: 2015-05
  serial-number:
    arxiv: '1505.04324'

Download: moura-2015-elaboration.bib · moura-2015-elaboration.yml

Cited by (1)

Elegant elaboration with function invocation zhang-2021-elegantarXiv · 2021

We present an elegant design of the core language in a dependently-typed lambda calculus with

𝛿

-reduction and an elaboration algorithm.

arXiv

Cites 35 works (1 here)

With notes (1)

Homotopy Type Theory: Univalent Foundations of Mathematics hottbookarXiv · 2013

Web · arXiv

External (34)

Theorem Proving in Lean (2016)
Constructing the propositional truncation using non-recursive HITs (2015)
The Lean Theorem Prover (2015)
Formalization of non-abelian topology for homotopy type theory (2015)
Experience Implementing a Performant Category-Theory Library in Coq (2014)
Canonical Structures for the Working Coq User (2013)
Idris, a general-purpose dependently typed programming language: design and implementation (2013)
Extending Hindley-Milner Type Inference with Coercive Structural Subtyping (2011)
The Matita Interactive Theorem Prover (2011)
Higher-Order Dynamic Pattern Unification for Dependent Types and Records (2011)
Type classes for mathematics in type theory† (2011)
Hints in Unification (2009)
A Brief Overview of Agda - A Functional Language with Dependent Types (2009)
Packaging Mathematical Structures (2009)
Programming in Higher-Order Logic (2009)
First-Class Type Classes (2008)
Handbook of Constraint Programming (2006)
Functional pearl: i am not a number–i am a free variable (2004)
Locales and Locale Expressions in Isabelle/Isar (2003)
Using Axiomatic Type Classes in Isabelle (2000)
Typing algorithm in type theory with inheritance (1997)
The Coq proof assistant reference manual: version 6.1 (1997)
Type classes in Haskell (1994)
Inductive families (1994)
Inductive Definitions in the system Coq - Rules and Properties (1993)
Investigations into intensional type theory (1993)
ECC, an extended calculus of constructions (1989)
The Calculus of Constructions (1988)
The Undecidability of the Second-Order Unification Problem (1981)
A Theory of Type Polymorphism in Programming (1978)
A unification algorithm for typed λ-calculus (1975)
An intuitionistic theory of types (1972)
The Principal Type-Scheme of an Object in Combinatory Logic (1969)
A predictable unification algorithm for Coq featuring universe polymorphism and overloading