Luigi Liquori and Simona Ronchi Della Rocca
Towards an intersection typed system
á la Church
In Proc. 3rd Int'l Workshop Intersection Types & Related
Systems (ITRS 2004), 2005
The ITRS '04 proceedings appears as vol. 136 (2005-07-19) of
Elec. Notes in Theoret. Comp. Sci.
In this paper, a fully typed lambda calculus based
on the well-known intersection type system
discipline is presented, based on a type store
storing informations about the structures of types
and a notion of modality, decorating terms,
remembering some informations about the structure of
the type assignment proof. The present system is the
counterpart á la Church of the type assignment
system as invented by Coppo and Dezani
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43