research-article

Proof-producing synthesis of ML from higher-order logic

Authors:

Magnus O. Myreen,

Scott OwensAuthors Info & Claims

ICFP '12: Proceedings of the 17th ACM SIGPLAN international conference on Functional programming

Pages 115 - 126

https://doi.org/10.1145/2364527.2364545

Published: 09 September 2012 Publication History

Abstract

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 pure 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 core subset of Standard ML, and have applied it to examples including functional data structures, a parser generator, cryptographic algorithms, and a garbage collector.

References

[1]

G. Barthe, D. Demange, and D. Pichardie. A formally verified SSA-based middle-end - Single Static Assignment meets CompCert. In H. Seidl, editor, 21st European Symposium on Programming, ESOP 2012, volume 7211 of LNCS, pages 47--66. Springer, 2012.

Digital Library

[2]

A. Barthwal and M. Norrish. Verified, executable parsing. In G. Castagna, editor, 18th European Symposium on Programming, ESOP 2009, volume 5502 of LNCS, pages 160--174. Springer, 2009.

Digital Library

[3]

R. S. Boyer and J. S. Moore. Proving theorems about LISP Functions. Journal of the Association for Computing Machinery, 22 (1): 129--144, 1975.

Digital Library

[4]

A. Charguéraud. Program verification through characteristic formulae. In Proceeding of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP 2010, pages 321--332. ACM, 2010.

Digital Library

[5]

A. Charguéraud. Characteristic formulae for the verification of imperative programs. In Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP 2011, pages 418--430. ACM, 2011.

Digital Library

[6]

A. Chlipala. A verified compiler for an impure functional language. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pages 93--106. ACM, 2010.

Digital Library

[7]

Coq. The Coq home page, 2012. http://coq.inria.fr/.

[8]

T. Coquand and G. Huet. The calculus of constructions. Inf. Comput., 76 (2-3): 95--120, Feb. 1988.

Digital Library

[9]

Z. Dargaye. Vèrification formelle d'un compilateur pour langages fonctionnels. D thesis, Universitè Paris 7 Diderot, July 2009.

[10]

J. Davis and M. O. Myreen. The self-verifying Milawa theorem prover is sound (down to the machine code that runs it), 2012. http://www.cl.cam.ac.uk/~mom22/jitawa/.

[11]

J. Duan, J. Hurd, G. Li, S. Owens, K. Slind, and J. Zhang. Functional correctness proofs of encryption algorithms. In G. Sutcliffe and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning: 12th International Conference, LPAR 2005, volume 3835 of LNAI, pages 519--533. Springer-Verlag, 2005.

Digital Library

[12]

M. Felleisen and D. P. Friedman. Control operators, the SECD-machine, and the lambda-calculus. In 3rd Working Conference on the Formal Description of Programming Concepts, Aug. 1986.

[13]

M. Felleisen, R. B. Findler, and M. Flatt. Semantics Engineering with PLT Redex. MIT Press, 2009.

Digital Library

[14]

J. Harrison. Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge, Cambridge, UK, 1995.

[15]

Hol. The HOL4 home page, 2012. http://hol.sourceforge.net/.

[16]

J. Hurd. Verification of the Miller-Rabin probabilistic primality test. J. Log. Algebr. Program., 56 (1-2): 3--21, 2003.

[17]

Isabelle. The Isabelle home page, 2012. http://www.cl.cam.ac.uk/research/hvg/isabelle/.

[18]

M. Kaufmann and J. S. Moore. The ACL2 home page, 2011. http://www.cs.utexas.edu/users/moore/acl2/.

[19]

A. Krauss. Automating Recursive Definitions and Termination Proofs in Higher-Order Logic. PhD thesis, Technische Universitiät München, 2009.

[20]

X. Leroy. A formally verified compiler back-end. J. Autom. Reasoning, 43 (4): 363--446, 2009.

Digital Library

[21]

X. Leroy and H. Grall. Coinductive big-step operational semantics. Inf. Comput., 207 (2): 284--304, 2009.

Digital Library

[22]

P. Letouzey. A new extraction for Coq. In Proceedings of the 2002 International Conference on Types for Proofs and Programs, TYPES'02, pages 200--219. Springer-Verlag, 2003.

Digital Library

[23]

G. Li. Validated compilation through logic. In M. Butler and W. Schulte, editors, FM 2011: Formal Methods - 17th International Symposium on Formal Methods, volume 6664 of LNCS, pages 169--183. Springer, 2011.

Digital Library

[24]

G. Li and K. Slind. Compilation as rewriting in higher order logic. In F. Pfenning, editor, Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, volume 4603 of LNCS, pages 19--34. Springer, 2007.

Digital Library

[25]

G. Li and K. Slind. Trusted source translation of a total function language. In C. R. Ramakrishnan and J. Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, volume 4963 of LNCS, pages 471--485. Springer, 2008.

Digital Library

[26]

G. Li, S. Owens, and K. Slind. Structure of a proof-producing compiler for a subset of higher order logic. In R. D. Nicola, editor, Programming Languages and Systems: 16th European Symposium on Programming, ESOP 2007, volume 4421 of LNCS, pages 205--219. Springer, 2007.

Digital Library

[27]

J. G. Malecha, G. Morrisett, A. Shinnar, and R. Wisnesky. Toward a verified relational database management system. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pages 237--248. ACM, 2010.

Digital Library

[28]

D. Matthews. Poly/ML home page, 2012. http://www.polyml.org.

[29]

A. McCreight, T. Chevalier, and A. P. Tolmach. A certified framework for compiling and executing garbage-collected languages. In Proceeding of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP 2010, pages 273--284, 2010.

Digital Library

[30]

R. Milner. Logic for computable functions; description of a machine implementation. Technical Report STAN-CS-72-288, A.I. Memo 169, Stanford University, 1972.

[31]

M. O. Myreen. Reusable verification of a copying collector. In G. T. Leavens, P. W. O'Hearn, and S. K. Rajamani, editors, Verified Software: Theories, Tools, Experiments, Third International Conference, VSTTE 2010, volume 6217 of LNCS, pages 142--156. Springer, 2010.

Digital Library

[32]

M. O. Myreen. Functional programs: conversions between deep and shallow embeddings. In L. Beringer and A. Felty, editors, Interactive Theorem Proving (ITP), volume 7406 of LNCS, pages 412--418. Springer, 2012.

[33]

M. O. Myreen and J. Davis. A verified runtime for a verified theorem prover. In M. C. J. D. van Eekelen, H. Geuvers, J. Schmaltz, and F. Wiedijk, editors, Interactive Theorem Proving (ITP), volume 6898 of LNCS, pages 265--280. Springer, 2011.

Digital Library

[34]

M. O. Myreen, K. Slind, and M. J. C. Gordon. Extensible proof-producing compilation. In O. de Moor and M. I. Schwartzbach, editors, Compiler Construction, 18th International Conference, CC 2009, volume 5501 of LNCS, pages 2--16. Springer, 2009.

Digital Library

[35]

M. Norrish and K. Slind. A thread of HOL development. Comput. J., 45 (1): 37--45, 2002.

[36]

C. Okasaki. Purely Functional Data Structures. Cambridge University Press, 1998.

Digital Library

[37]

S. Owens and K. Slind. Adapting functional programs to higher-order logic. Higher-Order and Symbolic Computation, 21 (4): 377--409, Dec. 2008.

Digital Library

[38]

J. Ševčik, V. Vafeiadis, F. Z. Nardelli, S. Jagannathan, and P. Sewell. Relaxed-memory concurrency and verified compilation. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, pages 43--54. ACM, 2011.

Digital Library

[39]

K. Slind. Reasoning about Terminating Functional Programs. PhD thesis, TU Munich, 1999.

[40]

K. Slind, S. Owens, J. Iyoda, and M. Gordon. Proof producing synthesis of arithmetic and cryptographic hardware. Formal Aspects of Computing, 19 (3): 343--362, Aug. 2007.

Digital Library

[41]

A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Inf. Comput., 115 (1): 38--94, 1994.

Digital Library

Cited By

Forster YSozeau MTabareau N(2024)Verified Extraction from Coq to OCamlProceedings of the ACM on Programming Languages10.1145/36563798:PLDI(52-75)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656379
Yuan SBesson FTalpin J(2024)End-to-End Mechanized Proof of a JIT-Accelerated eBPF Virtual Machine for IoTComputer Aided Verification10.1007/978-3-031-65627-9_16(325-347)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65627-9_16
Yuan SLion BBesson FTalpin J(2023)Making an eBPF Virtual Machine Faster on Microcontrollers: Verified Optimization and Proof SimplificationDependable Software Engineering. Theories, Tools, and Applications10.1007/978-981-99-8664-4_22(385-401)Online publication date: 27-Nov-2023
https://dl.acm.org/doi/10.1007/978-981-99-8664-4_22
Show More Cited By

Index Terms

Proof-producing synthesis of ML from higher-order logic
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods

Recommendations

Proof-producing synthesis of ML from higher-order logic
ICFP '12

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 pure functional programs. However, to efficiently run these programs, they must be converted (or "...
Self-Formalisation of Higher-Order Logic

We present a mechanised semantics for higher-order logic (HOL), and a proof of soundness for the inference system, including the rules for making definitions, implemented by the kernel of the HOL Light theorem prover. Our work extends Harrison's ...
Proving Isomorphism of First-Order Logic Proof Systems in HOL

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP '12: Proceedings of the 17th ACM SIGPLAN international conference on Functional programming

September 2012

392 pages

ISBN:9781450310543

DOI:10.1145/2364527

General Chair:
Peter Thiemann
University of Freiburg, Germany
,
Program Chair:
Robby Findler
Northwestern University, USA

ACM SIGPLAN Notices Volume 47, Issue 9
ICFP '12
September 2012
368 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2398856
Issue’s Table of Contents

Copyright © 2012 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 September 2012

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tag

theorem proving

Qualifiers

Research-article

Conference

ICFP'12

Sponsor:

SIGPLAN

ICFP'12: ACM SIGPLAN International Conference on Functional Programming

September 9 - 15, 2012

Copenhagen, Denmark

Acceptance Rates

ICFP '12 Paper Acceptance Rate 32 of 88 submissions, 36%;

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

18
Total Citations
View Citations
211
Total Downloads

Downloads (Last 12 months)3
Downloads (Last 6 weeks)0

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Forster YSozeau MTabareau N(2024)Verified Extraction from Coq to OCamlProceedings of the ACM on Programming Languages10.1145/36563798:PLDI(52-75)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656379
Yuan SBesson FTalpin J(2024)End-to-End Mechanized Proof of a JIT-Accelerated eBPF Virtual Machine for IoTComputer Aided Verification10.1007/978-3-031-65627-9_16(325-347)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65627-9_16
Yuan SLion BBesson FTalpin J(2023)Making an eBPF Virtual Machine Faster on Microcontrollers: Verified Optimization and Proof SimplificationDependable Software Engineering. Theories, Tools, and Applications10.1007/978-981-99-8664-4_22(385-401)Online publication date: 27-Nov-2023
https://dl.acm.org/doi/10.1007/978-981-99-8664-4_22
Cruz-Filipe LLugović LMontesi F(2023)Certified Compilation of Choreographies with haccFormal Techniques for Distributed Objects, Components, and Systems10.1007/978-3-031-35355-0_3(29-36)Online publication date: 10-Jun-2023
https://doi.org/10.1007/978-3-031-35355-0_3
Pit-Claudel CPhilipoom JJamner DErbsen AChlipala AJhala RDillig I(2022)Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level codeProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523706(918-933)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523706
Pit-Claudel CWang PDelaware BGross JChlipala A(2020)Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and ProofsAutomated Reasoning10.1007/978-3-030-51054-1_7(119-137)Online publication date: 24-Jun-2020
https://doi.org/10.1007/978-3-030-51054-1_7
Chajed TTassarotti JKaashoek MZeldovich NBrecht TWilliamson C(2019)Verifying concurrent, crash-safe systems with PerennialProceedings of the 27th ACM Symposium on Operating Systems Principles10.1145/3341301.3359632(243-258)Online publication date: 27-Oct-2019
https://dl.acm.org/doi/10.1145/3341301.3359632
Becker HZyuzin NMonat RDarulova EMyreen MFox A(2018)A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL42018 Formal Methods in Computer Aided Design (FMCAD)10.23919/FMCAD.2018.8603019(1-10)Online publication date: Oct-2018
https://doi.org/10.23919/FMCAD.2018.8603019
Bohrer RTan YMitsch SMyreen MPlatzer A(2018)VeriPhy: verified controller executables from verified cyber-physical system modelsACM SIGPLAN Notices10.1145/3296979.319240653:4(617-630)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3296979.3192406
Bohrer RTan YMitsch SMyreen MPlatzer AFoster JGrossman D(2018)VeriPhy: verified controller executables from verified cyber-physical system modelsProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3192366.3192406(617-630)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3192366.3192406
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents