Authors: Dougherty, Daniel
Ghilezan, Silvia 
Lescanne, Pierre
Title: Intersection and union types in the λ̄μμ̃-calculus
Journal: Electronic Notes in Theoretical Computer Science
Volume: 136
First page: 153
Last page: 172
Conference: 3rd International Workshop on intersection Types and Related Systems; 13 July 2004 through 13 July 2004
Issue Date: 19-Jul-2005
ISSN: 1571-0661
DOI: 10.1016/j.entcs.2005.06.010
Abstract: 
The original λ̄μμ̃ of Curien and Herbelin has a system of simple types, based on sequent calculus, embodying a Curry-Howard correspondence with classical logic. We introduce and discuss three type assignment systems that are extensions of λ̄μμ̃ with intersection and union types. The intrinsic symmetry in the λ̄μ μ̃ calculus leads to an essential use of both intersection and union types.
Keywords: Classical logic | Curry-Howard correspondence | Intersection types | Union types | λ̄μμ̃-calculus
Publisher: Elsevier

Show full item record

SCOPUSTM   
Citations

4
checked on Jun 15, 2024

Page view(s)

44
checked on May 9, 2024

Google ScholarTM

Check

Altmetric

Altmetric


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