Pure type systems and classical sequents

Abstract

(eng) The bar lambda mu tilde mu-calculus was designed by P.-L. Curien and H. Herbelin. One of its interest is that its terms can be interpreted as derivations in the classical sequent calculus. One of the its lacks is the fact that it has only simple types. Our purpose here is to extend the calculus to higher-order types, and especially those of the calculus of constructions, a calculus designed by T. Coquand and G. Huet in order to provide a very general typed language for proof assistants based on \lambda-calculus. In order to do this, we place ourselves in the framework of pure type systems, which are a very general formalism allowing to represent many interesting type systems, among which those of Barendregt's lambda-cube, which is a hierarchical presentation of the calculus of constructions. We show that our systems satisfy some fundamental properties, such as subject reduction, and strong normalisation on the lambda-cube.