Abstract
Few programming languages have a mathematically rigorous definition or metatheory—in part because they are perceived as too large and complex to work with. This paper demonstrates the feasibility of such undertakings: we formalize a substantial portion of the semantics of Objective Caml’s core language (which had not previously been given a formal semantics), and we develop a mechanized type soundness proof in HOL. We also develop an executable version of the operational semantics, verify that it coincides with our semantic definition, and use it to test conformance between the semantics and the OCaml implementation. We intend our semantics to be a suitable substrate for the verification of OCaml programs.
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
Kahrs, S.: Mistakes and ambiguities in the definition of Standard ML. Technical Report ECS-LFCS-93-257, University of Edinburgh (April 1993)
Rossberg, A.: Defects in the revised definition of Standard ML. Technical report, Saarland University, Saarbrücken, Germany (October 2001), Updated 2007/01/22
Leroy, X.: The Objective Caml System. 3.10 edn. (2007) http://caml.inria.fr/pub/docs/manual-ocaml/index.html .
Sewell, P., Zappa Nardelli, F., Owens, S., Peskine, G., Ridge, T., Sarkar, S., Strniša, R.: Ott: Effective tool support for the working semanticist. In: Proc. ICFP (2007)
Norrish, M., Slind, K.: HOL-4, http://hol.sourceforge.net/
Slind, K.: Reasoning about Terminating Functional Programs. PhD thesis, Institut für Informatik, Technische Universität München (1999)
Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Proc. Design and Application of Strategies/Tactics in Higher Order Logics (2003)
Compton, M.: Stenning’s protocol implemented in UDP and verified in Isabelle. In: Proc. Australasian Symposium on Theory of Computing (2005)
Liu, H., Moore, J.S.: Java program verification via a JVM deep embedding in ACL2. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, Springer, Heidelberg (2004)
Ridge, T.: Operational reasoning for concurrent Caml programs and weak memory models. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, Springer, Heidelberg (2007)
Aydemir, B.E., Bohannon, A., Fairbairn, M., Foster, J.N., Pierce, B.C., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S., Zdancewic, S.: Mechanized metatheory for the masses: The POPLmark Challenge. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, Springer, Heidelberg (2005)
Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. Trans. on Prog. Lang. and Systems 28(4), 619–695 (2006)
Lee, D.K., Crary, K., Harper, R.: Towards a mechanized metatheory of Standard ML. In: Proc. Principles of Programming Languages (2007)
Maharaj, S., Gunter, E.L.: Studying the ML module system in HOL. In: Melham, T.F., Camilleri, J. (eds.) HUG 1994. LNCS, vol. 859, Springer, Heidelberg (1994)
Nipkow, T., van Oheimb, D.: Java light is type-safe — definitely. In: POPL (1998)
Norrish, M.: C Formalised in HOL. PhD thesis, University of Cambridge (1998)
Syme, D.: Reasoning with the formal definition of Standard ML in HOL. In: Joyce, J.J., Seger, C.-J.H. (eds.) HUG 1993. LNCS, vol. 780, Springer, Heidelberg (1994)
Syme, D.: Proving Java type soundness. In: Formal Syntax and Semantics of Java, pp. 83–118. Springer, Heidelberg (1999)
VanInwegen, M.: The Machine-Assisted Proof of Programming Language Properties. PhD thesis, University of Pennsylvania (1996)
Harper, R.: personal correspondence (2007)
Harper, R., Licata, D.: Mechanizing metatheory in a logical framework. Journal of Functional Programming 17(4–5), 613–673 (2007)
Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). MIT Press, Cambridge (1997)
Matthews, J., Findler, R.B.: An operational semantics for Scheme. Journal of Functional Programming (to appear)
Moore, J.S.: Symbolic simulation: An ACL2 approach. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, Springer, Heidelberg (1998)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Owens, S. (2008). A Sound Semantics for OCaml light . In: Drossopoulou, S. (eds) Programming Languages and Systems. ESOP 2008. Lecture Notes in Computer Science, vol 4960. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78739-6_1
Download citation
DOI: https://doi.org/10.1007/978-3-540-78739-6_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78738-9
Online ISBN: 978-3-540-78739-6
eBook Packages: Computer ScienceComputer Science (R0)