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.
pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.