Towards an Intersection Typed System à la Church

Luigi Liquori (1, 2) , Simona Ronchi Della Rocca (3)

1 MIRHO - Objects, types and prototypes : semantics and validation
2 LOGNET - Logical Networks: Self-organizing Overlay Networks and Programmable Overlay Computing Systems
3 Dipartimento di Informatica [Torino]

In this paper, we presents a comfortable fully typed lambda calculus based on the well-known intersection type system discipline where proof are not only feasible but easy; the present system is the counterpart à la Church of the type assignment system as invented by Coppo and Dezani.

Mots clés: Typed lambda calculus; Intersection types; Church type assignment system; Curry-Howard correspondence

Domaines: Informatique et langage [cs.CL]; Logique en informatique [cs.LO]

Luigi Liquori, Simona Ronchi Della Rocca. Towards an Intersection Typed System à la Church. Proceedings of the Third International Workshop on Intersection Types and Related Systems (ITRS 2004) Intersection Types and Related Systems 2004, Jul 2004, Turku, Finland. pp.43-56, ⟨10.1016/j.entcs.2005.06.015⟩. ⟨hal-01149611⟩