Towards a mechanized metatheory of standard ML

ABSTRACT

We present an internal language with equivalent expressive power to Standard ML, and discuss its formalization in LF and the machine-checked verification of its type safety in Twelf. The internal language is intended to serve as the target of elaboration in an elaborative semantics for Standard ML in the style of Harper and Stone. Therefore, it includes all the programming mechanisms necessary to implement Standard ML, including translucent modules, abstraction, polymorphism, higher kinds, references, exceptions, recursive types, and recursive functions. Our successful formalization of the proof involved a careful interplay between the precise formulations of the various mechanisms, and required the invention of new representation and proof techniques of general interest.

REFERENCES

• 1: H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. Elsevier, 1984.
• 2: Karl Crary and Susmit Sarkar. Foundational certified code in a metalogical framework. In Nineteenth International Conference on Automated Deduction, Miami, Florida, 2003. Extended version published as CMU technical report CMU-CS-03-108.
• 3: Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582176]
• 4: Joëlle Despeyroux , Amy P. Felty , André Hirschowitz, Higher-Order Abstract Syntax in Coq, Proceedings of the Second International Conference on Typed Lambda Calculi and Applications, p.124-138, April 10-12, 1995
• 5: Derek Dreyer , Robert Harper , Karl Crary, Understanding and evolving the ml module system, Carnegie Mellon University, Pittsburgh, PA, 2005
• 6: Derek Dreyer , Karl Crary , Robert Harper, A type system for higher-order modules, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.236-249, January 15-17, 2003, New Orleans, Louisiana, USA
• 7: Derek Dreyer, Robert Harper, Manuel M.T. Chakravarty, and Gabriele Keller. Modular type classes. Technical Report TR-2006-03, University of Chicago, April 2006.
• 8: Sophia Drossopoulou and Susan Eisenbach. Towards an operational semantics and proof of type soundness for Java. In Formal Syntax and Semantics of Java. Springer-Verlag, March 1998.
• 9: Sophia Drossopoulou, Tanya Valkevych, and Susan Eisenbach. Java type soundness revisited, September 2000 Technical report, Imperial College London.
• 10: M. J. C. Gordon , T. F. Melham, Introduction to HOL: a theorem proving environment for higher order logic, Cambridge University Press, New York, NY, 1993
• 11: Robert Harper, A simplified account of polymorphic references, Information Processing Letters, v.51 n.4, p.201-206, Aug. 24, 1994 [doi>10.1016/0020-0190(94)90120-1]
• 12: Robert Harper , Furio Honsell , Gordon Plotkin, A framework for defining logics, Journal of the ACM (JACM), v.40 n.1, p.143-184, Jan. 1993 [doi>10.1145/138027.138060]
• 13: Robert Harper and Daniel R. Licata. Mechanizing language definitions. Submitted for publication, April 2006.
• 14: Robert Harper , Mark Lillibridge, A type-theoretic approach to higher-order modules with sharing, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.123-137, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.176927]
• 15: Robert Harper , John C. Mitchell , Eugenio Moggi, Higher-order modules and the phase distinction, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.341-354, December 1989, San Francisco, California, United States [doi>10.1145/96709.96744]
• 16: Robert Harper , Christopher Stone, A type-theoretic interpretation of standard ML, Proof, language, and interaction: essays in honour of Robin Milner, MIT Press, Cambridge, MA, 2000
• 17: Gerwin Klein and Tobias Nipkow. A machine-checked model for a Java-like language, virtual machine and compiler. Technical Report 0400001T.1, National ICT Australia, Sydney, March 2004.
• 18: Daniel K. Lee, Karl Crary, and Robert Harper. Mechanizing the metatheory of Standard ML. Technical Report CMU-CS-06-138, Carnegie Mellon University, School of Computer Science, 2006.
• 19: Xavier Leroy, Manifest types, modules, and separate compilation, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.109-122, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.176926]
• 20: Xavier Leroy, Applicative functors and fully transparent higher-order modules, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.142-153, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199476]
• 21: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• 22: Greg Morrisett , Matthias Felleisen , Robert Harper, Abstract models of memory management, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.66-77, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224182]
• 23: L. C. Paulson, The foundation of a generic theorem prover, Journal of Automated Reasoning, v.5 n.3, p.363-397, September 1989 [doi>10.1007/BF00248324]
• 24: Leaf Eames Petersen , Robert Harper, Certifying compilation for standard ml in a type analysis framework, Carnegie Mellon University, Pittsburgh, PA, 2005
• 25: Leaf Petersen, Perry Cheng, Robert Harper, and Chris Stone. Implementing the TILT internal language. Technical Report CMU-CS-00-180, Carnegie Mellon University, School of Computer Science, December 2000.
• 26: Frank Pfenning. Computation and deduction. Lecture notes, available electronically at http://www.cs.cmu.edu/char"7Etwelf.
• 27: Frank Pfenning and Carsten Schürmann. Twelf User's Guide, Version 1.4, 2002. Available electronically at http://www.cs.cmu.edu/char"7Etwelf.
• 28: Brigitte Pientka and Frank Pfenning. Termination and reduction checking in the logical framework. In Workshop of Automation of Proofs by Mathematical Induction, June 2000.
• 29: Benjamin Pierce , Martin Steffen, Higher-order subtyping, Theoretical Computer Science, v.176 n.1-2, p.235-282, April 20, 1997 [doi>10.1016/S0304-3975(96)00096-5]
• 30: Benjamin C. Pierce, Types and programming languages, MIT Press, Cambridge, MA, 2002
• 31: Gordon D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, University of Aarhus, 1981.
• 32: John C. Reynolds. The essence of Algol. In J. W. de Bakker and J. C. van Vliet, editors, Proceedings of the International Symposium on Algorithmic Languages, pages 345--372, Amsterdam, October 1981. North-Holland.
• 33: Jeffrey Sarnat and Carsten Schürmann. A proof-theoretic account of logical relations. Submitted for publication, 2006.
• 34: Christopher Allan Stone , Robert Harper, Singleton kinds and singleton types, 2000
• 35: Christopher A. Stone , Robert Harper, Extensional equivalence and singleton types, ACM Transactions on Computational Logic (TOCL), v.7 n.4, p.676-722, October 2006
• 36: Don Syme, Reasoning with the Formal Definition of Standard ML in HOL, Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications, p.43-60, August 11-13, 1993
• 37: D. Tarditi , G. Morrisett , P. Cheng , C. Stone , R. Harper , P. Lee, TIL: a type-directed optimizing compiler for ML, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.181-192, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 38: Myra Ellen Vaninwegen , Carl Gunter, The machine-assisted proof of programming language properties, 1996
• 39: Myra Van Inwegen , Elsa L. Gunter, HOL-ML, Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications, p.61-74, August 11-13, 1993
• 40: Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. A concurrent logical framework: The propositional fragment. In S. Berardi, M. Coppo, and F. Damiani, editors, Types for Proofs and Programs, volume 3085 of Lecture Notes in Computer Science, pages 355--377. Springer-Verlag, 2004. Papers from the Third International Workshop on Types for Proofs and Programs, April 2003, Torino, Italy.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Syntax

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

General Terms:
Languages, Verification

Keywords:
language definitions, logical frameworks, mechanized metatheory, standard ML, twelf, type safety