Skip to main content

Questions tagged [bound-variables]

Bound variables refer to variables that serve as a placeholder to point to a binder. In calculus, "∫ t dx" is a binder and any free appearance of the variable "x" in "t" is bound.

Filter by
Sorted by
Tagged with
10 votes
5 answers
2k views

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

There are many possible ways to represent syntax with variable binding, such as named variables, De Bruijn indices, De Bruijn levels, locally nameless terms, nominal type theories, etc. There are also ...
10 votes
1 answer
251 views

Performance of de Bruijn indices?

Can any of you refer me to documented results of experiments on the performance of provers using de Bruijn indices to represent references to bound variables versus mentions of names or other simple ...