## Elaine Pimentel, Simona Ronchi della Rocca, and Luca Roversi.
Towards a proof-theoretical justification for intersection types.
Technical report, Dipartimento di Informatica, Università di
Torino, 2004.

It is well known that derivations in Intersection
Types (IT) form a strict subset of deductions in
Intuitionistic Logic (LJ) - up to term decorations -
in the sense that IT imposes a meta-theoretical
restriction on proofs: conjunction can be introduced
only between derivations that are synchronized with
respect to the implication. The goal of this work is to
present a proof-theoretical justification for IT. In
particular, we discuss the relationship between the
intersection connective and the intuitionistic
conjunction. For this purpose, we define a new logical
system called Intersection Synchronous Logic (ISL),
that proves properties of sets of deductions of the
implication-conjunction fragment of LJ. The main idea
behind ISL is the decomposition of the intuitionistic
conjunction into two connectives, one with synchronous
and the other with asynchronous behavior. Also in the
present work, we prove that ISL enjoys both the strong
normalization and sub-formula properties as well as
that the Intersection Type assignment can be viewed as
standard term decoration of ISL.

[ bib |
http ]

Back

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