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 | 9112 reads
|
Browse archivesActive forum topics |
Recent comments
8 weeks 3 days ago
8 weeks 5 days ago
8 weeks 6 days ago
15 weeks 6 days ago
21 weeks 4 days ago
21 weeks 5 days ago
22 weeks 4 days ago
25 weeks 2 days ago
26 weeks 5 days ago
26 weeks 6 days ago