Proof-Producing Synthesis of CakeML from Monadic HOL Functions

被引：8

作者：

Abrahamsson, Oskar ^{[1
]}

Ho, Son ^{[2
]}

Kanabar, Hrutvik ^{[3
]}

Kumar, Ramana ^{[4
]}

Myreen, Magnus O. ^{[1
]}

Norrish, Michael ^{[5
]}

Tan, Yong Kiam ^{[6
]}

机构：

[1] Chalmers Univ Technol, Gothenburg, Sweden

[2] PSL Res Univ, MINES ParisTech, Paris, France

[3] Univ Kent, Canterbury, Kent, England

[4] DeepMind, London, England

[5] Australian Natl Univ, CSIRO, Data61, Canberra, ACT, Australia

[6] Carnegie Mellon Univ, Pittsburgh, PA 15213 USA

来源：

JOURNAL OF AUTOMATED REASONING | 2020年 / 64卷 / 07期

关键词：

Interactive theorem proving; Program synthesis; ML; Higher-order logic; HIGHER-ORDER LOGIC;

D O I：

10.1007/s10817-020-09559-8

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

We introduce an automatic method for producing stateful ML programs together with proofs of correctness from monadic functions in HOL. Our mechanism supports references, exceptions, and I/O operations, and can generate functions manipulating local state, which can then be encapsulated for use in a pure context. We apply this approach to several non-trivial examples, including the instruction encoder and register allocator of the otherwise pure CakeML compiler, which now benefits from better runtime performance. This development has been carried out in the HOL4 theorem prover.

引用

页码：1287 / 1306

页数：20

共 16 条

[1]

Anand Abhishek, 2017, CoqPL

[2]

Anand Abhishek., 2018, CoqPL

[3]

Blazy S., 2010, LNCS, V6012

[4]

Bulwahn L, 2008, LECT NOTES COMPUT SC, V5170, P134, DOI 10.1007/978-3-540-71067-7_14

[5] Verified Characteristic Formulae for CakeML [J].

Gueneau, Armael ;

Myreen, Magnus O. ;

Kumar, Ramana ;

Norrish, Michael .

PROGRAMMING LANGUAGES AND SYSTEMS (ESOP 2017): 26TH EUROPEAN SYMPOSIUM ON PROGRAMMING, 2017, 10201 :584-610

[6] Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions [J].

Ho, Son ;

Abrahamsson, Oskar ;

Kumar, Ramana ;

Myreen, Magnus O. ;

Tan, Yong Kiam ;

Norrish, Michael .

AUTOMATED REASONING, IJCAR 2018, 2018, 10900 :646-662

[7]

Hupel L., 2018, EUR S PROGR ESOP

[8]

Hurd J, 2011, LECT NOTES COMPUT SC, V6617, P177, DOI 10.1007/978-3-642-20398-5_14

[9] Self-Formalisation of Higher-Order Logic Semantics, Soundness, and a Verified Implementation [J].

Kumar, Ramana ;

Arthan, Rob ;

Myreen, Magnus O. ;

Owens, Scott .

JOURNAL OF AUTOMATED REASONING, 2016, 56 (03) :221-259

[10] CakeML: A Verified Implementation of ML [J].

Kumar, Ramana ;

Myreen, Magnus O. ;

Norrish, Michael ;

Owens, Scott .

ACM SIGPLAN NOTICES, 2014, 49 (01) :179-191

← 1 2 →