Pottinger, Garrel The Church-Rosser theorem for the typed \(\lambda\)-calculus with surjective pairing. (English) Zbl 0423.03009 Notre Dame J. Formal Logic (to appear). Page: −5 −4 −3 −2 −1 ±0 +1 +2 +3 +4 +5 Show Scanned Page Cited in 1 ReviewCited in 2 Documents MSC: 03B40 Combinatory logic and lambda calculus Keywords:Church-Rosser theorem; typed and type-free combinatory systems; typed lambda-calculus with pairing and projection constants PDFBibTeX XML