Sound and Complete Typing for lambda-mu
Logic in Computer Science
2011-01-25 v1
Abstract
In this paper we define intersection and union type assignment for Parigot's calculus lambda-mu. We show that this notion is complete (i.e. closed under subject-expansion), and show also that it is sound (i.e. closed under subject-reduction). This implies that this notion of intersection-union type assignment is suitable to define a semantics.
Cite
@article{arxiv.1101.4425,
title = {Sound and Complete Typing for lambda-mu},
author = {Steffen van Bakel},
journal= {arXiv preprint arXiv:1101.4425},
year = {2011}
}
Comments
In Proceedings ITRS 2010, arXiv:1101.4104