User loginNavigation |
A New Approach to Abstract Syntax with Variable BindingPitts and Gabbay, A New Approach to Abstract Syntax with Variable Binding, FAC 2001. In the lambda calculus, the particular choice of variable names - even free variables - is irrelevant. Names serve two purposes:
In a theory of binders, only the latter purpose is relevant. This is why it's so annoying to have to deal with capture-avoiding substitution, the Barendregt variable convention,
There are several standard ways to deal with this. Generating fresh names with This paper introduces a theory of fresh names that restores algebraic reasoning, referential transparency, and structural induction to algebraic datatypes with a HOAS-like notation for introducing binders into an abstract syntax. This is the set-theoretical basis for the authors' work on FreshML and FreshO'Caml, which we've discussed a little bit on LtU in the past. By Dave Herman at 2005-03-14 15:53 | Lambda Calculus | Meta-Programming | Theory | other blogs | 9571 reads
|
Browse archives
Active forum topics |
Recent comments
6 weeks 15 hours ago
6 weeks 19 hours ago
6 weeks 19 hours ago
28 weeks 2 days ago
32 weeks 3 days ago
34 weeks 1 day ago
34 weeks 1 day ago
36 weeks 5 days ago
41 weeks 3 days ago
41 weeks 3 days ago