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 

Pimentel+Ronchi+Roversi:2012-FI (Article)
Author(s) Elaine Pimentel, Simonetta Ronchi Della Rocca and Luca Roversi
Title« Intersection Types from a proof-theoretic perspective »
JournalFundamenta Informaticae
Volume121
Number1-4
Page(s)253 --- 274
Year2012
URLhttp://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2012-FI/PimentelRonchiRoversi2012FI.pdf
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.

BibTeX code

@article{Pimentel+Ronchi+Roversi:2012-FI,
  number = {1-4},
  volume = {121},
  month = {Dicember},
  author = {Pimentel, Elaine and {Ronchi della Rocca}, Simonetta and Roversi,
            Luca},
  url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2012-FI/PimentelRonchiRoversi2012FI.pdf},
  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.},
  title = {Intersection Types from a proof-theoretic perspective},
  year = {2012},
  pages = {253 --- 274},
  journal = {{F}undamenta {I}nformaticae},
}


 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!