Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadata
Contributor : Luigi Liquori Connect in order to contact the contributor
Submitted on : Tuesday, November 26, 2013 - 2:10:07 PM
Last modification on : Saturday, January 27, 2018 - 1:30:59 AM
Long-term archiving on: : Thursday, February 27, 2014 - 9:50:32 AM


Files produced by the author(s)




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⟩



Les métriques sont temporairement indisponibles