Sciweavers

Share
LPAR
2010
Springer

Logic and Computation in a Lambda Calculus with Intersection and Union Types

8 years 3 months ago
Logic and Computation in a Lambda Calculus with Intersection and Union Types
We present an explicitly typed lambda calculus "`a la Church" based on the union and intersection types discipline; this system is the counterpart of the standard type assignment calculus "`a la Curry." Our typed calculus enjoys Subject Reduction and confluence, and typed terms are strongly normalizing 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.
Daniel J. Dougherty, Luigi Liquori
Added 14 Feb 2011
Updated 14 Feb 2011
Type Journal
Year 2010
Where LPAR
Authors Daniel J. Dougherty, Luigi Liquori
Comments (0)
books