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

Abstract : 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.
Type de document :
Communication dans un congrès
Edmund M. Clarke and Andrei Voronkov. 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. Springer, 6355, pp.173-191, 2010, Lecture Notes in Computer Science. 〈10.1007/978-3-642-17511-4_11〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00909535
Contributeur : Luigi Liquori <>
Soumis le : mardi 26 novembre 2013 - 14:10:07
Dernière modification le : samedi 27 janvier 2018 - 01:30:59
Document(s) archivé(s) le : jeudi 27 février 2014 - 09:50:32

Fichier

lpar.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Daniel J. Dougherty, Luigi Liquori. Logic and computation in a lambda calculus with intersection and union types. Edmund M. Clarke and Andrei Voronkov. 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. Springer, 6355, pp.173-191, 2010, Lecture Notes in Computer Science. 〈10.1007/978-3-642-17511-4_11〉. 〈hal-00909535〉

Partager

Métriques

Consultations de la notice

340

Téléchargements de fichiers

127