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

Browse archives
Active forum topics

Recent comments
13 weeks 3 days ago
17 weeks 5 days ago
19 weeks 2 days ago
19 weeks 2 days ago
22 weeks 16 hours ago
26 weeks 5 days ago
26 weeks 5 days ago
27 weeks 1 day ago
27 weeks 1 day ago
29 weeks 6 days ago