Computing Publications

Publications Home » Approaches to Polymorphism in Cla...

Approaches to Polymorphism in Classical Sequent Calculus

Alexander Summers, Steffen van Bakel

Conference or Workshop Paper
ESOP 2006
March, 2006
Springer Verlag

X is a relatively new, untyped 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 lambda-calculus, Bloo and Rose's lambda-x, Parigot's lambda-mu and Curien and Herbelin's lambda-bar-mu-mu-tilde.

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. A type-assignment algorithm is defined for this system, which generalises Milner's W.

PDF of full publication (158 kilobytes)
(need help viewing PDF files?)
BibTEX file for the publication
Conditions for downloading publications from this site. built & maintained by Ashok Argent-Katwala.