Proof-producing synthesis of ML from higher-order logic

8 years 2 months ago
Proof-producing synthesis of ML from higher-order logic
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 logica...
Magnus O. Myreen, Scott Owens
Added 29 Sep 2012
Updated 29 Sep 2012
Type Journal
Year 2012
Where ICFP
Authors Magnus O. Myreen, Scott Owens
Comments (0)