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.
Summers, A. J., & Van Bakel, S. (2006). Approaches to polymorphism in classical sequent calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3924 LNCS, pp. 84–99). https://doi.org/10.1007/11693024_7