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 captureavoiding 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 HOASlike notation for introducing binders into an abstract syntax. This is the settheoretical 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 20050314 15:53  Lambda Calculus  MetaProgramming  Theory  other blogs  7800 reads

Browse archivesActive forum topics 
Recent comments
1 hour 34 min ago
3 hours 9 min ago
3 hours 26 min ago
9 hours 46 min ago
11 hours 43 min ago
21 hours 15 min ago
21 hours 53 min ago
23 hours 11 min ago
23 hours 24 min ago
1 day 3 hours ago