## Simona Ronchi Della Rocca and Luca Roversi.
Intersection Logic.
In *Proceedings of CSL'01*, volume 2412 of *Lecture Notes
in Computer Science*, pages 414 - 428. Springer Verlag, 2001.

The intersection type assignment system IT uses the
formulas of the negative fragment of the predicate
calculus (LJ) as types for the terms. However, the
deductions of IT only correspond to the proper subset
of the derivations of LJ obtained by imposing a
meta-theoretic condition about the use of the
conjunction of LJ. This paper proposes a logical
foundation for IT. This is done by introducing a logic
IL. Intuitively, a derivation of IL is a set of
derivations in LJ such that the derivations in the set
can be thought of as writable in parallel. This way of
looking at LJ, by means of IL, means that the
meta-theoretic condition mentioned above can be
transformed into a purely structural property of IL.
The relation between IL and LJ surely has a first main
benefit: the strong normalization of LJ directly
implies the same property on IL, which translates into
a very simple proof of the strong normalizability of
the terms typable with IT.

[ bib |
http ]

Back

*This file has been generated by
bibtex2html 1.60*
>>> BackToHomePage(Protocollo) <<<