Logic and computation in a lambda calculus with intersection and union types - Archive ouverte HAL Access content directly
Conference Papers Year : 2010

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

(1) , (2)
1
2

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.
Fichier principal
Vignette du fichier
lpar.pdf (152.29 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

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

Identifiers

Cite

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 View
115 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More