Skip to main content

New answers tagged

4 votes

How do real-world proof assistants bind variables and check equality?

Agda Variables in Agda are represented as de Bruijn indices, and there is a type of explicit substitutions that is used in many places throughout the typechecker. Reduction is done by a lazy abstract ...
6 votes

How do real-world proof assistants bind variables and check equality?

Since you asked about Lean, it uses De Bruijn indices and naive/explicit substitution for bound variables, unique names/locally nameless for free variables, and call by name with caching. The ...
6 votes

How do real-world proof assistants bind variables and check equality?

Core term definition In the latest version of Aya, we use locally nameless approach where names are represented by Java object identity (see this), and bound variables are integers (see this). Bound ...
7 votes

How do real-world proof assistants bind variables and check equality?

Idris 2 is self-hosted and as such it can use dependent types when specifying the operations on its own intermediate representations. Variables The core language is well-scoped by construction which ...
8 votes

How do real-world proof assistants bind variables and check equality?

Variables λΠ uses the Bindlib library, and so do several other systems, see the paper Abstract Representation of Binders in OCaml using the Bindlib Library and package documentation. I have recently ...
7 votes

Possible root cause(s) of the misunderstanding that DTT implies not Turing complete?

[Supplemental: I rewrote the answer so that any shred of vagueness is gone, as it was evoking religuous zeal, and I would prefer to stick to math. Everything is explained in terms of a widely accepted ...
Andrej Bauer's user avatar
  • 9,593
5 votes

Possible root cause(s) of the misunderstanding that DTT implies not Turing complete?

Is this perhaps a problem with 'common understanding' regarding what it means to be Turing complete? Indeed it is: a pop-science understanding of dependent types has led to this myth being deeply ...
gallais's user avatar
  • 1,256

Top 50 recent answers are included