User loginNavigation 
Barendregt's ConventionHi, I am doing some proofs on a calculus with existential types and I am fairly liberally applying Baredregt's convention (approximately that bound variables are distinctly named). My assumption is that I have to justify using this convention and that that justification is along the lines of 'the rules of the calculus abide by the convention'. However, I can not find any information about a formal way of justifying this. Does anyone have experience of this, or pointers to relavent papers? Thanks, Nick By nick cameron at 20080201 11:02  LtU Forum  previous forum topic  next forum topic  other blogs  5621 reads

Browse archivesActive forum topics 
Recent comments
13 hours 45 min ago
15 hours 13 min ago
15 hours 41 min ago
1 day 21 hours ago
1 day 22 hours ago
2 days 16 hours ago
2 days 18 hours ago
2 days 18 hours ago
3 days 10 hours ago
3 days 11 hours ago