Reduction in X does not agree with Intersection and Union Types (Extended abstract)

Autor:	van Bakel, Steffen
Rok vydání:	2011
Předmět:	Computer Science - Logic in Computer Science
Druh dokumentu:	Working Paper
Popis:	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. Comment: 4th International Workshop on Intersection Types and Related Systems (ITRS'08), Turin, Italy, March 2008
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/1109.4570 Zobrazit plný text záznamu View this record from Arxiv