Proof-Producing Synthesis of ML from Higher-Order Logic

Myreen, Magnus O. and Owens, Scott (2012) Proof-Producing Synthesis of ML from Higher-Order Logic. In: ICFP '12: 17th ACM SIGPLAN International Conference on Functional Programming, September 10th - 12th, 2012, Copenhagen, Denmark. (The full text of this publication is not available from this repository)

The full text of this publication is not available from this repository. (Contact us about this Publication)
Official URL
http://dx.doi.org/10.1145/2364527.2364545

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.

Item Type: Conference or workshop item (Paper)
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Programming Languages and Systems Group
Depositing User: Scott Owens
Date Deposited: 24 Oct 2012 09:59
Last Modified: 18 Mar 2013 14:12
Resource URI: http://kar.kent.ac.uk/id/eprint/31890 (The current URI for this page, for reference purposes)
  • Depositors only (login required):