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 | 9318 reads
|
Browse archivesActive forum topics |
Recent comments
5 days 4 hours ago
4 weeks 6 days ago
5 weeks 3 days ago
5 weeks 3 days ago
7 weeks 3 days ago
7 weeks 3 days ago
7 weeks 6 days ago
7 weeks 6 days ago
8 weeks 6 days ago
9 weeks 5 days ago