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

SCOPUSTM   
Citations

2
checked on Jun 15, 2024

Page view(s)

46
checked on May 9, 2024

Google ScholarTM

Check

Altmetric

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.