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.

Downloads

Download data is not yet available.

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: 02 july 2020. doi: https://doi.org/10.26686/ajl.v6i0.1792.