Logic and computation in a lambda calculus with intersection and union types - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2010

Logic and computation in a lambda calculus with intersection and union types

Résumé

We present an explicitly typed lambda calculus "à la Church" based on the union and intersection types discipline; this system is the counterpart of the standard type assignment calculus "à la Curry." Our typed calculus enjoys Subject Reduction and confluence, and typed terms are strongly normal- izing when the universal type is omitted. Moreover both type checking and type reconstruction are decidable. In contrast to other typed calculi, a system with union types will fail to be "coherent" in the sense of Tannen, Coquand, Gunter, and Scedrov: different proofs of the same typing judgment will not necessarily have the same meaning. In response, we introduce a decidable notion of equality on type-assignment derivations inspired by the equational theory of bicartesian-closed categories.
Fichier principal
Vignette du fichier
lpar.pdf (152.29 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-00909535 , version 1 (26-11-2013)

Identifiants

Citer

Daniel J. Dougherty, Luigi Liquori. Logic and computation in a lambda calculus with intersection and union types. 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-16, Dakar, Senegal, April 25–May 1, 2010, Revised Selected Papers, Apr 2010, Dakar, Senegal. pp.173-191, ⟨10.1007/978-3-642-17511-4_11⟩. ⟨hal-00909535⟩

Collections

INRIA INRIA2
103 Consultations
124 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More