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  7620 reads

Browse archivesActive forum topics 
Recent comments
24 min 44 sec ago
1 hour 13 min ago
7 hours 47 min ago
9 hours 31 min ago
17 hours 48 min ago
17 hours 48 min ago
18 hours 24 min ago
19 hours 59 min ago
22 hours 17 min ago
1 day 1 hour ago