Affiliations: Departamento de Matematicas, Universidad del Valle, Colombia. [email protected] | Dipartimento di Informatica, Università di Torino, Italy. [email protected] | Dipartimento di Informatica, Università di Torino, Italy. [email protected]
Note: [] Work partially supported by CNPq and FAPEMIG. Address for correspondence: Departamento de Matematicas, Universidad del Valle, Colombia and Departamento de Matematica, Universidade Federal de Minas Gerais, Brazil
Note: [] Work partially supported by PRIN '07 CONCERTO.
Note: [] WAddress for correspondence: Departamento de Matematicas, Universidad del Valle, Colombia and Departamento de Matematica, Universidade Federal de Minas Gerais, Brazil
Abstract: In this work we present a proof-theoretical justification for the intersection type assignment system (IT) by means of the logical system Intersection Synchronous Logic (ISL). ISL builds classes of equivalent deductions of the implicative and conjunctive fragment of the intuitionistic logic (NJ). ISL results from decomposing intuitionistic conjunction into two connectives: a synchronous conjunction, that can be used only among equivalent deductions of NJ, and an asynchronous one, that can be applied among any sets of deductions of NJ. A term decoration of ISL exists so that it matches both: the IT assignment system, when only the synchronous conjunction is used, and the simple types assignment with pairs and projections, when the asynchronous conjunction is used. Moreover, the proof of strong normalization property for ISL is a simple consequence of the same property in NJ and hence strong normalization for IT comes for free.
Keywords: Intersection types, λ-calculus, type assignment systems, structural proof-theory
