arXiv Analytics

Sign in

arXiv:0905.2545 [math.LO]AbstractReferencesReviewsResources

A direct proof of the confluence of combinatory strong reduction

René David

Published 2009-05-15Version 1

I give a proof of the confluence of combinatory strong reduction that does not use the one of lambda-calculus. I also give simple and direct proofs of a standardization theorem for this reduction and the strong normalization of simply typed terms.

Comments: To appear in TCS
Categories: math.LO, cs.LO
Related articles: Most relevant | Search more
arXiv:1012.0596 [math.LO] (Published 2010-12-02, updated 2016-03-01)
A direct proof of the five element basis theorem
arXiv:math/9405215 [math.LO] (Published 1994-05-15)
On a theorem of Shapiro
arXiv:1607.05237 [math.LO] (Published 2016-07-18)
A Direct Proof of Schwichtenberg's Bar Recursion Closure Theorem

Links

Toolbox