|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
checked on Mar 27, 2023
checked on Mar 28, 2023
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.