Sökning: id:"swepub:oai:research.chalmers.se:5b5bb0d3-1213-4e79-ae67-f1d180d9bdba" >
Proof-Producing Syn...
Proof-Producing Synthesis of CakeML from Monadic HOL Functions
-
- Abrahamsson, Oskar, 1986 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
- Ho, Son (författare)
- PSL University Paris
-
- Kanabar, Hrutvik (författare)
- University Of Kent
-
visa fler...
-
- Kumar, Ramana (författare)
- Google DeepMind
-
- Myreen, Magnus, 1983 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
- Norrish, Michael (författare)
- Australian National University
-
- Tan, Yong Kiam (författare)
- Carnegie Mellon University (CMU)
-
visa färre...
-
(creator_code:org_t)
- 2020-06-06
- 2020
- Engelska.
-
Ingår i: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 64:7, s. 1287-1306
- Relaterad länk:
-
https://research.cha... (primary) (free)
-
visa fler...
-
https://link.springe...
-
https://doi.org/10.1...
-
https://research.cha...
-
https://research.cha...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datorteknik (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Engineering (hsv//eng)
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
- NATURVETENSKAP -- Matematik -- Matematisk analys (hsv//swe)
- NATURAL SCIENCES -- Mathematics -- Mathematical Analysis (hsv//eng)
Nyckelord
- ML
- Interactive theorem proving
- Program synthesis
- Higher-order logic
Publikations- och innehållstyp
- art (ämneskategori)
- ref (ämneskategori)
Hitta via bibliotek
Till lärosätets databas