Unpublished

Abstract

Subject Reduction vs Intersection / Union Types in LambdaBar-Mu-Mutilde.
by S. van Bakel.

This paper defines intersection and union type assignment for the calculus LambdaBar-Mu-Mutilde [Curien-Herbelin'00], a proof-term syntax for Gentzen's classical sequent calculus. We show that this notion is closed for subject-expansion, and show that it needs to be restricted to satisfy subject-reduction as well, even when limiting reduction to (confluent) call-by-name or call-by-value reduction, making it unsuitable to define a semantics.

To appear in proceedings of Visions of Computer Science, British Computer Society's international academic conference, London, September 2008.

ps pdf