Hostname: page-component-66644f4456-mv4w6 Total loading time: 0 Render date: 2025-02-12T18:16:56.606Z Has data issue: true hasContentIssue false
  • English
  • Français

Proof-producing translation of higher-order logic into pure and stateful ML

Part of: JFP Research Articles

Published online by Cambridge University Press:  20 January 2014

MAGNUS O. MYREEN  and
SCOTT OWENS
MAGNUS O. MYREEN
Affiliation:
Computer Laboratory, University of Cambridge, Cambridge, UK (e-mail: [email protected])
SCOTT OWENS
Affiliation:
School of Computing, University of Kent, Canterbury, UK (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

The higher-order logic found in proof assistants such as Coq and various HOL systems provides a convenient setting for the development and verification of functional programs. However, to efficiently run these programs, they must be converted (or ‘extracted’) to functional programs in a programming language such as ML or Haskell. With current techniques, this step, which must be trusted, relates similar looking objects that have very different semantic definitions, such as the set-theoretic model of a logic and the operational semantics of a programming language. In this paper, we show how to increase the trustworthiness of this step with an automated technique. Given a functional program expressed in higher-order logic, our technique provides the corresponding program for a functional language defined with an operational semantics, and it provides a mechanically checked theorem relating the two. This theorem can then be used to transfer verified properties of the logical function to the program. We have implemented our technique in the HOL4 theorem prover, translating functions to a subset of Standard ML, and have applied the implementation to examples including functional data structures, a parser generator, cryptographic algorithms, a garbage collector and the 500-line kernel of the HOL light theorem prover. This paper extends our previous conference publication with new material that shows how functions defined in terms of a state-and-exception monad can be translated, with proofs, into stateful ML code. The HOL light example is also new.

Type
Articles
Information
Journal of Functional Programming , Volume 24 , Issue 2-3: ICFP 2012 , May 2014 , pp. 284 - 315
Copyright
Copyright © Cambridge University Press 2014 

References

Aydemir, B. E., Bohannon, A., Fairbairn, M., Foster, J. N., Pierce, B. C., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S. & Zdancewic, S. (2005) Mechanized metatheory for the masses: The PoplMark challenge. In Theorem Proving in Higher Order Logics (TPHOLs), Hurd, J. & Melham, T. F. (eds). Berlin: Springer, pp. 50–65.CrossRefGoogle Scholar
Barthe, G., Demange, D. & Pichardie, D. (2012) A formally verified SSA-based middle-end: Static single assignment meets CompCert. In Proceedings of European Symposium on Programming (ESOP '12), Seidl, H. (ed), vol. 7211. Berlin: Springer, pp. 47–66.Google Scholar
Barthwal, A. & Norrish, M. (2009) Verified, executable parsing. In Proceedings of European Symposium on Programming (ESOP'09), Castagna, G. (ed), vol. 5502. Berlin: Springer, pp.160–174.Google Scholar
Boyer, R. S. & Moore, J. S. (1975) Proving theorems about LISP functions. J. Assoc. Comput. Mach. 22 (1), 129–144.CrossRefGoogle Scholar
Charguéraud, A. (2010) Program verification through characteristic formulae. In Proceedings of International Conference on Functional Programming (ICFP '10). New York: ACM, 321–332.Google Scholar
Charguéraud, A. (2011) Characteristic formulae for the verification of imperative programs. In Proceedings of International Conference on Functional Programming (ICFP'11). New York: ACM, pp. 418–430.Google Scholar
Chlipala, A. (2010) A verified compiler for an impure functional language. In Proceedings of Principles of Programming Languages (POPL '10). New York: ACM, pp. 93–106.Google Scholar
Coquand, T. & Huet, G. (1988) The calculus of constructions. Inf. Comput. 76 (2–3), 95–120.CrossRefGoogle Scholar
Dargaye, Z. (2009) Vèrification formelle d'un compilateur pour langages fonctionnels. Paris: Universitè Paris 7 Diderot.Google Scholar
Davis, J. & Myreen, M. O. (2012) The Self-Verifying Milawa Theorem Prover is Sound (Down to the Machine Code that Runs it). Available at: http://www.cl.cam.ac.uk/~mom22/jitawa/ Accessed Nov 1, 2013.Google Scholar
Duan, J., Hurd, J., Li, G., Owens, S., Slind, K. & Zhang, J. (2005) Functional correctness proofs of encryption algorithms. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), Sutcliffe, G. & Voronkov, A. (eds). Berlin: Springer-Verlag, pp. 519–533.CrossRefGoogle Scholar
Harrison, J. (1995) Metatheory and Reflection in Theorem Proving: A Survey and Critique, Technical Report CRC-053. Cambridge, UK: SRI Cambridge.Google Scholar
Hurd, J. (2003) Verification of the Miller-Rabin probabilistic primality test. J. Log. Algebr. Program. 56 (1–2), 3–21.CrossRefGoogle Scholar
Krauss, A. (2009) Automating Recursive Definitions and Termination Proofs in Higher-Order Logic. Munich: Technische Universitiät München.Google Scholar
Kumar, R., Myreen, M. O., Norrish, M. & Owens, S. (2014) CakeML: A verified implementation of ML. In Principles of Programming Languages (POPL), Sewell, P. (ed). ACM.Google Scholar
Leroy, X. (2009) A formally verified compiler back-end. J. Autom. Reasoning 43 (4), 363–446.CrossRefGoogle Scholar
Letouzey, P. (2003) A new extraction for Coq. In Types for Proofs and Programs (TYPES). Berlin: Springer, pp. 200–219.CrossRefGoogle Scholar
Li, G. (2011) Validated compilation through logic. In Formal Methods (FM), Butler, M. & Schulte, W. (eds), vol. 6664. Berlin: Springer, pp. 169–183.Google Scholar
Li, G., Owens, S. & Slind, K. (2007) Structure of a proof-producing compiler for a subset of higher order logic. In European Symposium on Programming (ESOP), De Nicola, R. (ed). Berlin: Springer, pp. 205–219.Google Scholar
Li, G. & Slind, K. (2007) Compilation as rewriting in higher order logic. In Automated Deduction (CADE), Pfenning, F. (ed), vol. 4603. Berlin: Springer, pp. 19–34.CrossRefGoogle Scholar
Li, G. & Slind, K. (2008) Trusted source translation of a total function language. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Ramakrishnan, C. R. & Rehof, J. (eds), vol. 4963. Berlin: Springer, pp. 471–485.Google Scholar
Malecha, J. G., Morrisett, G., Shinnar, A. & Wisnesky, R. (2010) Toward a verified relational database management system. In Proceedings of Principles of Programming Languages (POPL'10). New York: ACM, pp. 237–248.Google Scholar
McCreight, A., Chevalier, T. & Tolmach, A. P. (2010) A certified framework for compiling and executing garbage-collected languages. In Proceedings of International Conference on Functional Programming (ICFP'10). New York: ACM, pp. 273–284.Google Scholar
Milner, R. (1972) Logic for Computable Functions: Description of a Machine Implementation, Technical Report STAN-CS-72-288, A.I. Memo 169. Stanford University.CrossRefGoogle Scholar
Milner, R., Tofte, M., Harper, R. & MacQueen, D. (1997) The Definition of Standard ML (Revised). Cambridge, MA: The MIT Press.CrossRefGoogle Scholar
Myreen, M. O. (2010) Reusable verification of a copying collector. In Verified Software: Theories, Tools, Experiments (VSTTE), Leavens, G. T., O'Hearn, P. W. & Rajamani, S. K. (eds). Berlin: Springer, pp. 142–156.CrossRefGoogle Scholar
Myreen, M. O. (2012) Functional programs: conversions between deep and shallow embeddings. In Interactive Theorem Proving (ITP), Beringer, L. & Felty, A. (eds), vol. 7406. Berlin: Springer, pp. 412–417.CrossRefGoogle Scholar
Myreen, M. O. & Curello, G. (2013) Proof pearl: A verified bignum implementation in x86-64 machine code. In Certified Programs and Proofs (CPP). Cham, Switzerland: Springer, pp. 66–81.CrossRefGoogle Scholar
Myreen, M. O. & Davis, J. (2011) A verified runtime for a verified theorem prover. In Interactive Theorem Proving (ITP), van Eekelen, M. C. J. D., Geuvers, H., Schmaltz, J. & Wiedijk, F. (eds), vol. 6898. Berlin: Springer, pp. 265–280.CrossRefGoogle Scholar
Myreen, M. O. & Owens, S. (2012) Proof-producing synthesis of ML from higher-order logic. In Proceedings of International Conference on Functional Programming (ICFP'12). New York: ACM, pp. 115–126.Google Scholar
Myreen, M. O., Owens, S., & Kumar, R. (2013) Steps towards verified implementations of HOL Light. In Interactive Theorem Proving (ITP), Blazy, S., Paulin-Mohring, C., & Pichardie, D. (eds). Berlin: Springer, pp. 490–495.CrossRefGoogle Scholar
Myreen, M. O., Slind, K. & Gordon, M. J. C. (2009) Extensible proof-producing compilation. In Compiler Construction (CC), de Moor, O. & Schwartzbach, M. I. (eds). Berlin: Springer, pp. 2–16.CrossRefGoogle Scholar
Norrish, M. & Slind, K. (2002) A thread of HOL development. Comput. J. 45 (1), 37–45.CrossRefGoogle Scholar
Okasaki, C. (1998) Purely Functional Data Structures. Cambridge, UK: Cambridge University.CrossRefGoogle Scholar
Owens, S. & Slind, K. (2008) Adapting functional programs to higher-order logic. Higher-order Symb. Comput. 21 (4), 377–409.CrossRefGoogle Scholar
Ševčík, J., Vafeiadis, V., Nardelli, F. Z., Jagannathan, S. & Sewell, P. (2011) Relaxed-memory concurrency and verified compilation. In Proceedings of Principles of Programming Languages (POPL'11). New York: ACM, pp. 43–54.Google Scholar
Slind, K. (1999) Reasoning about Terminating Functional Programs, PhD Thesis. Technical University of Munich.Google Scholar
Slind, K., Owens, S., Iyoda, J. & Gordon, M. (2007) Proof producing synthesis of arithmetic and cryptographic hardware. Form. Asp. Comput. 19 (3), 343–362.CrossRefGoogle Scholar
Submit a response

Discussions

No Discussions have been published for this article.