Abstract |
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. |
@inproceedings{Ronchi+Roversi:2001-CSL,
volume = {2412},
author = {Ronchi Della Rocca, Simona and Roversi, Luca},
series = {Lecture Notes in Computer Science},
booktitle = {Proceedings of CSL'01},
url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2001-CSL/RonchiRoversi2001CSL.ps.gz},
title = {Intersection {L}ogic},
abstract = {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. },
copyrightspringer = {http://www.springer.de/comp/lncs/index.html},
publisher = {Springer Verlag},
pages = {414--428},
year = {2001},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)