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. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.45.2 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |