Characterizing strong normalization in a language with control operators.
Résumé
We investigate some fundamental properties of the reduction relation in the untyped term calculus derived from Curien and Herbelin's lambda-mu-mu~. The original lambda-mu-mu~ has a system of simple types, based on sequent calculus, embodying a Curry-Howard correspondence with classical logic; the significance of the untyped calculus of raw terms is that it is a Turing-complete language for computation with explicit representation of control as well as code. We define a type assignment system for the raw terms satisfying: a term is typable if and only if it is strongly normalizing. The intrinsic symmetry in the lambda-mu-mu~ calculus leads to an essential use of both intersection and union types; in contrast to other union-types systems in the literature, our system enjoys the Subject Reduction property.
Nous examinons quelques propriétés fondamentales de la relation de réduction dans le calcul sans types dérivé du calcul λμμ de Curien et Herbelin. Le calcul originel λμμ possède un système de type simple fondés sur le calcul des séquents et impliquant une correspondance de Curry-Howard avec la logique classique. Le calcul sans type,dit des termes bruts,est un langage complet au sens de Turing qui contient une représentation explicite du contrôle aussi bien que du code et c’est cela sa spécificité. Nous définissons sur ces termes bruts un système de types qui satisfait la condition suivante:un terme est typable si et seulement si il est fortement normalisable. La symétrie intrinsèque de λμμ conduit a une utilisation essentielle de l’union et de l’intersection dans les types.Contrairement à ceux que rapporte la littérature, notre système a la propriété de réduction du sujet.
| Origine | Fichiers produits par l'(les) auteur(s) |
|---|
Loading...