Reduction in X does not agree with Intersection and Union Types (Extended abstract)
Logic in Computer Science
2011-09-22 v1
Abstract
This paper defines intersection and union type assignment for the calculus X, a substitution free language that enjoys the Curry-Howard correspondence with respect to Gentzen's sequent calculus for classical logic. We show that this notion is closed for subject-expansion, and show that it needs to be restricted to satisfy subject-reduction as well, making it unsuitable to define a semantics.
Cite
@article{arxiv.1109.4570,
title = {Reduction in X does not agree with Intersection and Union Types (Extended abstract)},
author = {Steffen van Bakel},
journal= {arXiv preprint arXiv:1109.4570},
year = {2011}
}
Comments
4th International Workshop on Intersection Types and Related Systems (ITRS'08), Turin, Italy, March 2008