Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
9655877 | Electronic Notes in Theoretical Computer Science | 2005 | 20 Pages |
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Daniel J. Dougherty, Silvia Ghilezan, Pierre Lescanne,