TY - GEN
T1 - A translation of intersection and union types for the λμ-calculus
AU - Kikuchi, Kentaro
AU - Sakurai, Takafumi
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2014.
PY - 2014
Y1 - 2014
N2 - We introduce an intersection and union type system for the λμ-calculus, which includes a restricted version of the traditional unionelimination rule. We give a translation from intersection and union types into intersection and product types, which is a variant of negative translation from classical logic to intuitionistic logic and naturally reflects the structure of strict intersection and union types. It is shown that a derivation in our type system can be translated into a derivation in the type system of van Bakel, Barbanera and de’Liguoro. As a corollary, the terms typable in our system turn out to be strongly normalising. We also present an intersection and union type system in the style of sequent calculus, and show that the terms typable in the system coincide with the strongly normalising terms of the λμ-calculus, a call-by-name fragment of Curien and Herbelin’s λμ˜μ-calculus.
AB - We introduce an intersection and union type system for the λμ-calculus, which includes a restricted version of the traditional unionelimination rule. We give a translation from intersection and union types into intersection and product types, which is a variant of negative translation from classical logic to intuitionistic logic and naturally reflects the structure of strict intersection and union types. It is shown that a derivation in our type system can be translated into a derivation in the type system of van Bakel, Barbanera and de’Liguoro. As a corollary, the terms typable in our system turn out to be strongly normalising. We also present an intersection and union type system in the style of sequent calculus, and show that the terms typable in the system coincide with the strongly normalising terms of the λμ-calculus, a call-by-name fragment of Curien and Herbelin’s λμ˜μ-calculus.
UR - http://www.scopus.com/inward/record.url?scp=84910006791&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84910006791&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-12736-1_7
DO - 10.1007/978-3-319-12736-1_7
M3 - Conference contribution
AN - SCOPUS:84910006791
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 120
EP - 139
BT - Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Proceedings
A2 - Garrigue, Jacques
PB - Springer Verlag
T2 - 12th Asian Symposium on Programming Languages and Systems, APLAS 2014
Y2 - 17 November 2014 through 19 November 2014
ER -