Computing Publications

Publications Home » Intersection and Union Types for X

Intersection and Union Types for X

Steffen van Bakel

Conference or Workshop Paper
3nd International Workshop on Intersection Types and Related Systems (ITRS'04), Turku, Finland
July, 2004
Electronic Notes in Theoretical Computer Science
Volume 136
pp.203–227
Elsevier
DOI 10.1016/j.entcs.2005.06.009
Abstract

This paper presents a notion of intersection and union type assignment for the calculus X, a substitution free language that can be used to describe the behaviour of functional programming languages at a very low level of granularity, and has first been defined in cite{Lengrand'03,vBLL'04}. X has been designed to give a Curry-Howard-de Bruijn correspondence to the sequent calculus for classical logic. In this paper we will define a notion of sequent-style intersection type assignment on X that needs union types, and show that this notion is closed for both subject-reduction and subject-expansion. We will also show that it is an extension of the Strict system for the Lambda Calculus.

PDF of full publication (219 kilobytes)
(need help viewing PDF files?)
BibTEX file for the publication
N.B.
Conditions for downloading publications from this site.
 

pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.