Questions tagged [binders]
Questions regarding binders (eg. by means of De Bruijn indices, HOAS, nominal approach) should be tagged with this.
6
questions
5
votes
2
answers
231
views
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 ...
- 429
5
votes
1
answer
320
views
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 ...
- 2,868
2
votes
1
answer
247
views
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 ...
- 2,868
3
votes
1
answer
156
views
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 ...
- 2,868
3
votes
0
answers
69
views
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 ...
18
votes
2
answers
398
views
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 ...
- 1,128