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 2008-02-01 11:02 | LtU Forum | previous forum topic | next forum topic | other blogs | 7704 reads
|
Browse archives
Active forum topics
|
Recent comments
11 weeks 13 hours ago
15 weeks 2 days ago
16 weeks 6 days ago
16 weeks 6 days ago
19 weeks 4 days ago
24 weeks 1 day ago
24 weeks 1 day ago
24 weeks 4 days ago
24 weeks 4 days ago
27 weeks 3 days ago