A presentation of the intersection type discipline through principal typings of normal forms (bibtex)
by Emilie Sayag, Michel Mauny
Abstract:
iffrenchNous introduisons un système de types intersection qui est une restriction des systèmes de types intersection classiques. Cette restriction conduit à la propriété de typage principal au sens classique pour les formes normales tout en gardant l'expressivité des systèmes de classiques. Nous caractérisons complètement la structure des types principaux des formes normales et nous donnons un algorithme de reconstruction d'une forme normale à partir d'un type principal. Ayant montré l'équivalence entre notion de type principal et les formes normales, nous définissons une opération d'expansion qui permet, composée avec l'opération de substitution, de retrouver tous les types possibles pour un $\lambda$-terme normalisable. La contribution de ce travail est la nouveauté et la simplicité de la présentation des types intersection à travers une notion de types principaux purement syntaxique et complètement caractérisée.We introduce an intersection type system which is a restriction of the intersection type discipline. This restriction leads to a principal type property for normal forms in the classical sense, while retaining the expressivity of the classical discipline. We characterize the structure of principal types of normal forms and give an algorithm that reconstructs normal forms from types. Having shown the equivalence between principal types and normal forms, we define an expansion operation on types which allows us to recover all possible types for any normalizable $\lambda$-term. The contribution of this work is a new and simpler presentation of the intersection type discipline through a purely syntactic and completely characterized notion of principal types.
Reference:
E. Sayag, M. Mauny, "A presentation of the intersection type discipline through principal typings of normal forms", INRIA, Rep. RR-2998, 1996.
Bibtex Entry:
@TechReport{Sayag-Mauny-1996b,
  author =       {Emilie Sayag and Michel Mauny},
  title =        {A presentation of the intersection type discipline
                  through principal typings of normal forms},
  institution =  {INRIA},
   year =         1996,
  number =       {RR-2998},
  abstract = {\iffrench{Nous introduisons un système de types
                  intersection qui est une restriction des systèmes
                  de types intersection classiques. Cette restriction
                  conduit à la propriété de typage principal au sens
                  classique pour les formes normales tout en gardant
                  l'expressivité des systèmes de classiques. Nous
                  caractérisons complètement la structure des types
                  principaux des formes normales et nous donnons un
                  algorithme de reconstruction d'une forme normale à
                  partir d'un type principal. Ayant montré
                  l'équivalence entre notion de type principal et les
                  formes normales, nous définissons une opération
                  d'expansion qui permet, composée avec l'opération de
                  substitution, de retrouver tous les types possibles
                  pour un $\lambda$-terme normalisable. La
                  contribution de ce travail est la nouveauté et la
                  simplicité de la présentation des types intersection
                  à travers une notion de types principaux purement
                  syntaxique et complètement caractérisée.}{We
                  introduce an intersection type system which is a
                  restriction of the intersection type
                  discipline. This restriction leads to a principal
                  type property for normal forms in the classical
                  sense, while retaining the expressivity of the
                  classical discipline. We characterize the structure
                  of principal types of normal forms and give an
                  algorithm that reconstructs normal forms from
                  types. Having shown the equivalence between
                  principal types and normal forms, we define an
                  expansion operation on types which allows us to
                  recover all possible types for any normalizable
                  $\lambda$-term. The contribution of this work is a
                  new and simpler presentation of the intersection
                  type discipline through a purely syntactic and
                  completely characterized notion of principal
                  types.}},
  url = {http://www.mauny.net/data/papers/sayag-mauny-1996b.pdf}
}
Powered by bibtexbrowser