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