A translation of intersection and union types for the λμ-calculus

Kentaro Kikuchi, Takafumi Sakurai

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationProgramming Languages and Systems - 12th Asian Symposium, APLAS 2014, Proceedings
EditorsJacques Garrigue
PublisherSpringer Verlag
Pages120-139
Number of pages20
ISBN (Electronic)9783319127354
DOIs
Publication statusPublished - 2014
Event12th Asian Symposium on Programming Languages and Systems, APLAS 2014 - Singapore, Singapore
Duration: 2014 Nov 172014 Nov 19

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8858
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other12th Asian Symposium on Programming Languages and Systems, APLAS 2014
CountrySingapore
CitySingapore
Period14/11/1714/11/19

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A translation of intersection and union types for the λμ-calculus'. Together they form a unique fingerprint.

Cite this