Approaches to polymorphism in classical sequent calculus

Abstract

X is a relatively new calculus, invented to give a Curry-Howard correspondence with Classical Implicative Sequent Calculus. It is already known to provide a very expressive language; embeddings have been defined of the λ-calculus, Bloo and Rose's λx, Parigot's λμ and Curien and Herbelin's λ̄μμ̄. We investigate various notions of polymorphism in the context of the X-calculus. In particular, we examine the first class polymorphism of System F, and the shallow polymorphism of ML. We define analogous systems based on the X-calculus, and show that these are suitable for embedding the original calculi. In the case of shallow polymorphism we obtain a more general calculus than ML, while retaining its useful properties. A type-assignment algorithm is defined for this system, which generalises Milner's W. © Springer-Verlag Berlin Heidelberg 2006.