Classical Sequents and Computation: An Overview
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.
Full text