Classical Sequents and Computation: An Overview

Steffen van Bakel
Department of Computing, Imperial College London


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.

Full text