Affordable Access

Une généralisation de la théorie des types en $\lambda$-calcul

Authors
Publication Date
Disciplines
  • Logic
  • Mathematics
  • Physics

Abstract

Une généralisation de la théorie des types en -calcul RAIRO INFORMATIQUE THÉORIQUE PATRICK SALLÉ Une généralisation de la théorie des types en λ-calcul RAIRO – Informatique théorique, tome 14, no 2 (1980), p. 143-167. <http://www.numdam.org/item?id=ITA_1980__14_2_143_0> © AFCET, 1980, tous droits réservés. L’accès aux archives de la revue « RAIRO – Informatique théorique » im- plique l’accord avec les conditions générales d’utilisation (http://www.numdam. org/legal.php). Toute utilisation commerciale ou impression systématique est constitutive d’une infraction pénale. Toute copie ou impression de ce fichier doit contenir la présente mention de copyright. Article numérisé dans le cadre du programme Numérisation de documents anciens mathématiques http://www.numdam.org/ R.A.l.R.O. Informatique théorique/Theoretical Informaties (voi. 14, n° 2, 1980, p. 143 à .167) UNE GÉNÉRALISATION DE LA THÉORIE DES TYPES EN À-CALCUL (Première partie) (*) par Patrick SALLE (*) Communiqué par J.-F. PERROT Résumé. — Nous décrivons une généralisation de la théorie des types de Curry qui étend Vaffectation de type à l'ensemble du X-calcul. Dans cette théorie deux expressions P-r| convertibles ont le même ensemble de types et une expression typée possède suivant la valeur de son type une forme normale ou une forme normale gauche. Abstract. — We present a gêneralization ofCurry's type theory which extends type assignment to the whole ofX-calculus. In our theory, any two expressions that are p-r\ convertible have the same set of types. Also, the value ofthe type of any typed expression indicates whether the expression possesses a normal form or a head normal form. INTRODUCTION Nous proposons une théorie des types sur le I-calcul qui est un outil pour les preuves d'arrêt et d'équivalence des programmes. Dans cette théorie un système de déduction composé d'axiomes et de règles d'inférences fournit un moyen mécanique d'obtention des types d'une expression. L'intérêt d'une théorie des t

There are no comments yet on this publication. Be the first to share your thoughts.