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

Browse archivesActive forum topics 
Recent comments
1 week 3 hours ago
1 week 1 day ago
1 week 1 day ago
2 weeks 4 days ago
2 weeks 4 days ago
2 weeks 5 days ago
2 weeks 5 days ago
2 weeks 5 days ago
2 weeks 5 days ago
2 weeks 5 days ago