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 

Ronchi+Roversi:2001-CSL (In proceedings)
Author(s) Simona Ronchi Della Rocca and Luca Roversi
Title« Intersection Logic »
InProceedings of CSL'01
SeriesLecture Notes in Computer Science
Volume2412
Page(s)414--428
Year2001
PublisherSpringer Verlag
URLhttp://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2001-CSL/RonchiRoversi2001CSL.ps.gz
Abstract
The intersection type assignment system IT uses the formulas of the negative fragment of the predicate calculus (LJ) as types for the terms. However, the deductions of IT only correspond to the proper subset of the derivations of LJ obtained by imposing a meta-theoretic condition about the use of the conjunction of LJ. This paper proposes a logical foundation for IT. This is done by introducing a logic IL. Intuitively, a derivation of IL is a set of derivations in LJ such that the derivations in the set can be thought of as writable in parallel. This way of looking at LJ, by means of IL, means that the meta-theoretic condition mentioned above can be transformed into a purely structural property of IL. The relation between IL and LJ surely has a first main benefit: the strong normalization of LJ directly implies the same property on IL, which translates into a very simple proof of the strong normalizability of the terms typable with IT.

BibTeX code

@inproceedings{Ronchi+Roversi:2001-CSL,
  volume = {2412},
  author = {Ronchi Della Rocca, Simona and Roversi, Luca},
  series = {Lecture Notes in Computer Science},
  booktitle = {Proceedings of CSL'01},
  url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2001-CSL/RonchiRoversi2001CSL.ps.gz},
  title = {Intersection {L}ogic},
  abstract = {The intersection type assignment system IT uses the formulas of
              the negative fragment of the predicate calculus (LJ) as types for
              the terms. However, the deductions of IT only correspond to the
              proper subset of the derivations of LJ obtained by imposing a
              meta-theoretic condition about the use of the conjunction of LJ.
              This paper proposes a logical foundation for IT. This is done by
              introducing a logic IL. Intuitively, a derivation of IL is a set
              of derivations in LJ such that the derivations in the set can be
              thought of as writable in parallel. This way of looking at LJ, by
              means of IL, means that the meta-theoretic condition mentioned
              above can be transformed into a purely structural property of IL.
              The relation between IL and LJ surely has a first main benefit:
              the strong normalization of LJ directly implies the same property
              on IL, which translates into a very simple proof of the strong
              normalizability of the terms typable with IT. },
  copyrightspringer = {http://www.springer.de/comp/lncs/index.html},
  publisher = {Springer Verlag},
  pages = {414--428},
  year = {2001},
}


 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!