Intersection Logic in sequent calculus style

Simona Ronchi Della Rocca
(Universita' di Torino Dipartimento di Informatica Torino Italy)
Alexis Saurin
(Laboratoire CNR PPS and INRIA Paris France)
Yiorgos Stavrinos
(Department of Mathematics, University of Athens, Greece)
Anastasia Veneti
(Department of Mathematics University of Athens Greece)

The intersection type assignment system has been designed directly as deductive system for assigning formulae of the implicative and conjunctive fragment of the intuitionistic logic to terms of lambda-calculus. But its relation with the logic is not standard. Between all the logics that have been proposed as its foundation, we consider ISL, which gives a logical interpretation of the intersection by splitting the intuitionistic conjunction into two connectives, with a local and global behaviour respectively, being the intersection the local one. We think ISL is a logic interesting by itself, and in order to support this claim we give a sequent calculus formulation of it, and we prove that it enjoys the cut elimination property.

Invited Presentation in Elaine Pimentel, Betti Venneri and Joe Wells: Proceedings Fifth Workshop on Intersection Types and Related Systems (ITRS 2010), Edinburgh, U.K., 9th July 2010, Electronic Proceedings in Theoretical Computer Science 45, pp. 16–30.
Published: 21st January 2011.

ArXived at: bibtex PDF

Comments and questions to:
For website issues: