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

Browse archivesActive forum topics 
Recent comments
3 hours 31 min ago
8 hours 30 min ago
8 hours 41 min ago
10 hours 46 min ago
17 hours 37 min ago
19 hours 9 min ago
22 hours 14 min ago
22 hours 27 min ago
22 hours 45 min ago
23 hours 29 min ago