Church-Rosser theorem for typed functional systems

DOI10.2307/2274330zbMath0583.03006OpenAlexW2031805453MaRDI QIDQ3707988

George Koletsos

Publication date: 1985

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2307/2274330

zbMATH Keywords

reductionrecursion operatortyped lambda calculusfunctional system of Girardinfinitely long terms

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items (7)

The metatheory of UTT ⋮ Behavioural inverse limit \(\lambda\)-models ⋮ Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves ⋮ Simplified Reducibility Proofs of Church-Rosser for β- and βη-reduction ⋮ Unnamed Item ⋮ Reducibility ⋮ Typing untyped \(\lambda\)-terms, or reducibility strikes again!

This page was built for publication: Church-Rosser theorem for typed functional systems