Abstract
We provide a strong normalization result for ML F, a type system generalizing ML with first-class polymorphism as in system F. The proof is achieved by translating ML F into a calculus of coercions, and showing that this calculus is just a decorated version of system F.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Milner, R., Tofte, M., Macqueen, D.: The definition of Standard ML. MIT Press, Cambridge (1997)
Girard, J.Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge tracts in theoretical computer science, vol. 7. Cambridge University Press, Cambridge (1989)
Le Botlan, D., Rémy, D.: MLF: Raising ML to the power of System F. In: Proc. of International Conference on Functional Programming (ICFP 2003), pp. 27–38 (2003)
Rémy, D., Yakobowski, B.: A Church-style intermediate language for MLF. Submitted (July 2009)
Leijen, D.: A type directed translation of MLF to System F. In: Proc. of International Conference on Functional Programming (ICFP 2007). ACM Press, New York (2007)
Botlan, D.L., Rémy, D.: Recasting MLF. Inf. Comput. 207(6), 726–785 (2009)
Barber, A., Plotkin, G.: Dual intuitionistic linear logic. Technical report LFCS-96-347, University of Edinburgh (1997)
Baillot, P., Terui, K.: Light types for polynomial time computation in lambda calculus. Inf. Comput. 207(1), 41–62 (2009)
Mitchell, J.C.: Coercion and type inference. In: Proc. of 11th Symposium on Principles of Programming Languages (POPL 1984), pp. 175–185. ACM, New York (1984)
Crary, K.: Typed compilation of inclusive subtyping. In: Proc. of International Conference on Functional Programming (ICFP 2000), pp. 68–81 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Manzonetto, G., Tranquilli, P. (2010). Harnessing ML F with the Power of System F . In: Hliněný, P., Kučera, A. (eds) Mathematical Foundations of Computer Science 2010. MFCS 2010. Lecture Notes in Computer Science, vol 6281. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15155-2_46
Download citation
DOI: https://doi.org/10.1007/978-3-642-15155-2_46
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15154-5
Online ISBN: 978-3-642-15155-2
eBook Packages: Computer ScienceComputer Science (R0)