Computing Publications

Publications Home » Intersection Types for lambda-Trees

Intersection Types for lambda-Trees

Steffen van Bakel, Franco Barbanera, Dezani Dezani-Ciancaglini, Fer-Jan de Vries

Journal Article
Theoretical Computer Science
Volume 272
Issues 1–2
pp.3–40
February, 2002
Elsevier
DOI 10.1016/S0304-3975(00)00346-7
Abstract

We introduce a type assignment system which is parametric with respect to five families of trees obtained by evaluating lambda-terms (Bohm trees, Levy-Longo trees, ...). Then we prove, in an (almost) uniform way, that each type assignment system fully describes the observational equivalences induced by the corresponding tree representation of terms. More precisely, for each family of trees, two terms have the same tree if and only if they get assigned the same types in the corresponding type assignment system.

PDF of full publication (325 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.