Abstract

This paper presents a short overview of some of the results achieved for the calculus X, which is based on Gentzen's LK. It presents the calculus, its suitability for encoding the lambda-calculus and the lambda-mu-calculus, as well as a type-preserving encoding of X into the pi-calculus.

Appeared as:

@InBook{Bakel-Barendregt60,

Author = "S. van Bakel",
Title = "Classical {S}equents and {C}omputation: an overview",
Publisher = "Radboud University Nijmegen",
Year = "2007"
}