Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

Pim+Ron+Rov:ITRS08 (Unpublished)
Author(s) E. Pimentel, S. Ronchi Della Rocca and L. Roversi
Title« Intersection Types from a proof-theoretic perspective »
URLhttp://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2008-ITRS/PMR-ITRS08.pdf
NotePresented at the 4th Workshop on Intersection Types and Related Systems (ITRS '08) -- Torino (Italy)
Abstract
In this work we present a proof-theoretical justification for IT by means of the logical system Intersection Synchronous Logic (ISL). ISL builds equivalence classes of deductions of the implicative and conjunctive fragment of 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

BibTeX code

@unpublished{Pim+Ron+Rov:ITRS08,
  month = {March},
  url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2008-ITRS/PMR-ITRS08.pdf},
  abstract = {In this work we present a proof-theoretical justification for IT
              by means of the logical system Intersection Synchronous Logic
              (ISL). ISL builds equivalence classes of deductions of the
              implicative and conjunctive fragment of 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},
  title = {{I}ntersection {T}ypes from a proof-theoretic perspective},
  author = {Pimentel, E. and Ronchi Della Rocca, S. and Roversi, L.},
  note = {Presented at the 4th Workshop on Intersection Types and Related
          Systems (ITRS '08) -- Torino (Italy)},
  year = {2008},
}


 Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)

Valid HTML 4.01!