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 

Ale+Dez+Lus:TCS-2004 (Article)
Author(s) Fabio Alessi, Mariangiola Dezani-Ciancaglini and Stefania Lusin
Title« Intersection Types and Domain Operators »
JournalTheoret. Comput. Sci.
Volume316
Number1--3
Page(s)25--47
Year2004
URLhttp://www.di.unito.it/~dezani/papers/adl.pdf
Abstract
We use intersection types as a tool for obtaining λ-models. Relying on the notion of easy intersection type theory we successfully build a λ-model in which the interpretation of an arbitrary simple easy term is any filter which can be described by a continuous predicate. This allows us to prove two results. The first gives a proof of consistency of the λ-theory where the λ-term (λ x.xx)(λ x.xx) is forced to behave as the join operator. This result has interesting consequences on the algebraic structure of the lattice of λ-theories. The second result is that for any simple easy term there is a λ-model where the interpretation of the term is the minimal fixed point operator.

BibTeX code

@article{Ale+Dez+Lus:TCS-2004,
  volume = {316},
  number = {1--3},
  author = {Alessi, Fabio and Dezani-Ciancaglini, Mariangiola and Lusin,
            Stefania},
  fjournal = {Theoretical Compututer Science},
  url = {http://www.di.unito.it/~dezani/papers/adl.pdf},
  title = {{Intersection Types and Domain Operators}},
  abstract = {We use intersection types as a tool for obtaining
              $\lambda$-models. Relying on the notion of {\em easy intersection
              type theory} we successfully build a $\lambda$-model in which the
              interpretation of an arbitrary simple easy term is any filter
              which can be described by a continuous predicate. This allows us
              to prove two results. The first gives a proof of consistency of
              the $\lambda$-theory where the $\lambda$-term $(\lambda
              x.xx)(\lambda x.xx)$ is forced to behave as the join operator.
              This result has interesting consequences on the algebraic
              structure of the lattice of $\lambda$-theories. The second result
              is that for any simple easy term there is a $\lambda$-model where
              the interpretation of the term is the {\em minimal} fixed point
              operator. },
  year = {2004},
  journal = {Theoret. Comput. Sci.},
  pages = {25--47},
}


 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!