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

Browse archivesActive forum topics 
Recent comments
23 hours 51 min ago
1 day 4 hours ago
2 days 4 hours ago
2 days 6 hours ago
2 days 12 hours ago
3 days 5 hours ago
3 days 14 hours ago
4 days 1 hour ago
4 days 2 hours ago
4 days 2 hours ago