Church-Rosser property and intersection types

  • George Koletsos Department of Computer Science, National Technical Univ. of Athens
  • George Stavrinos MPLA, Department of Mathematics, Univ. of Athens

Abstract

We give a proof via reducibility of the Church-Rosser property for the system D of λ-calculus with intersection types. As a consequence we can get the confluence property for developments directly, without making use of the strong normalization property for developments, by using only the typability in D and a suitable embedding of developments in this system. As an application we get a proof of the Church-Rosser theorem for the untyped λ-calculus.

Author Biographies

George Koletsos, Department of Computer Science, National Technical Univ. of Athens
George Stavrinos, MPLA, Department of Mathematics, Univ. of Athens
Published
2008-08-04
How to Cite
KOLETSOS, George; STAVRINOS, George. Church-Rosser property and intersection types. The Australasian Journal of Logic, [S.l.], v. 6, aug. 2008. ISSN 1448-5052. Available at: <https://ojs.victoria.ac.nz/ajl/article/view/1792>. Date accessed: 18 july 2019. doi: https://doi.org/10.26686/ajl.v6i0.1792.