Skip to main content

Questions tagged [binders]

Questions regarding binders (eg. by means of De Bruijn indices, HOAS, nominal approach) should be tagged with this.

Filter by
Sorted by
Tagged with
5 votes
2 answers

Algorithm for the locally nameless representation used by Lean

I have heard that Lean uses the locally nameless representation for handling binders, yet if I input an expression that has a bound variable in it, the bound variable is not displayed using its de ...
5 votes
1 answer

What is a weak function space and what does it have to do with HOAS?

What is a weak function space and what does it have to do with higher order abstract syntax? I mean I know what a weak function space is. It's that thing you use for HOAS in Lambda Prolog or toolkits ...
17 votes
2 answers

How to deal with Binders?

When reasoning about programming languages in a deep embedding, $\alpha$-equivalence, binders and capture-avoiding substitution quickly can become tedious. Complex binders may introduce multiple bound ...
2 votes
1 answer

Axiomization of Peano arithmetic in constructive first-order logic

I've been playing with axiomising systems of first-order logic in Coq. I've started to develop the beginning of a framework. As an example I give a minimal phrasing of Peano arithmetic in Coq in the ...
3 votes
1 answer

Is there a way to use higher order abstract syntax with linear types?

Is there a way to use HOAS style with linear types? I'm also interested in affine types or other substructural systems. I vaguely recall there has been some work for embedded DSLs for Haskell but I'm ...
3 votes
0 answers

Variable binding techniques used in proof assistants? [duplicate]

There are many resources (1, 2, 3, 4) to learn about various techniques for manipulating syntax with variable binding, however, I haven't seen many descriptions of which specific techniques are ...