Abstract
Advanced polymorphic type systems have come to play an important role in the world of functional programming. But, curiously, these type systems have so far had little impact upon widely-used imperative programming languages like C and C++. We show that ML-style polymorphism can be integrated smoothly into a dialect of C, which we call Polymorphic C. It has the same pointer operations as C, including the address-of operator &, the dereferencing operator*, and pointer arithmetic. Our type system allows these operations in their full generality, so that programmers need not give up the flexibility of C to gain the benefits of ML-style polymorphism. We prove a type soundness theorem that gives a rigorous and useful characterization of well-typed Polymorphic C programs in terms of what can go wrong when they are evaluated.
This material is based upon activities supported by the National Science Foundation under Agreements No. CCR-9414421 and CCR-9400592. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the authors and do not necessarily reflect the views of the National Science Foundation.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Damas, L. and Milner, R., Principal Type Schemes for Functional Programs, Proc. 9th ACM Symposium on Principles of Programming Languages, pp. 207–212, 1982.
Gordon, M., Milner, R. and Wadsworth, C., Edinburgh LCF, Lecture Notes in Computer Science 78, Springer-Verlag, 1979.
Gunter, C., Semantics of Programming Languages: Structures and Techniques, MIT Press, 1992.
Harper, R., A Simplified Account of Polymorphic References, Information Processing Letters, 51, pp. 201–206, August 1994.
Harper, R. and Morrisett, G., Compiling Polymorphism Using Intensional Type Analysis, Proc. 22nd ACM Symposium on Principles of Programming Languages, pp. 130–141, 1995.
Kernighan, B. and Ritchie, D., The C Programming Language, Prentice-Hall, 1978.
Leroy, X. and Weis, P., Polymorphic Type Inference and Assignment, Proc. 18th ACM Symposium on Principles of Programming Languages, pp. 291–302, 1991.
Leroy, X., Unboxed Objects and Polymorphic Typing, Proc. 19th ACM Symposium on Principles of Programming Languages, pp. 177–188, 1992.
Shao, Z. and Appel, A., A Typed-Based Compiler for Standard ML, Proc. 1995 Conf. on Programming Language Design and Implementation, pp. 116–129, 1995.
Standard ML of New Jersey, Version 0.93, February 15, 1993.
Tofte, M., Type Inference for Polymorphic References, Information and Computation, 89, pp. 1–34, 1990.
Volpano, D. and Smith, G., A Type Soundness Proof for Variables in LCF ML, Information Processing Letters, 56, pp. 141–146, November 1995.
Wright, A., Simple Imperative Polymorphism, Lisp and Symbolic Computation 8, 4 pp. 343–356, December 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Smith, G., Volpano, D. (1996). Towards an ML-style polymorphic type system for C. In: Nielson, H.R. (eds) Programming Languages and Systems — ESOP '96. ESOP 1996. Lecture Notes in Computer Science, vol 1058. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61055-3_47
Download citation
DOI: https://doi.org/10.1007/3-540-61055-3_47
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61055-7
Online ISBN: 978-3-540-49942-8
eBook Packages: Springer Book Archive