|Authors:||Ghilezan, Silvia||Title:||Inhabitation in intersection and union type assignment systems||Journal:||Journal of Logic and Computation||Volume:||3||Issue:||6||First page:||671||Last page:||685||Issue Date:||1-Dec-1993||ISSN:||0955-792X||DOI:||10.1093/logcom/3.6.671||Abstract:||
Union does not correspond to intuitionistic disjunction and intersection does not correspond to intuitionistic conjunction. The Curry-Howard isomorphism between types inhabited in the intersection and union type assignment system and formulae provable in intuitionistic propositional logic with implication, conjunction, disjunction and truth does not hold. This is shown semantically. The extension of the simply typed lambda calculus with conjunction and disjunction types and the corresponding elimination and introduction rules is considered. By the Curry-Howard isomorphism types inhabited in this extension of the simply typed lambda calculus correspond to the intuitionistically provable formulae. We shall link the inhabitation in the intersection and union type assignment system with the inhabitation in this extension of the simply typed lambda calculus.
|Keywords:||Curry-Howard isomorphism | Inhabitation | Intersection types | Intuitionistic propositional logic | Provability | Typed lambda calculus||Publisher:||Oxford University Press|
Show full item record
checked on Apr 1, 2023
checked on Apr 2, 2023
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.