Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant
We present Fiat, a library for the Coq proof assistant supporting refinement of declarative specifications into efficient functional programs with a high degree of automation. Each refinement process leaves a proof trail, checkable by the normal Coq kernel, justifying its soundness. We focus on the...
Main Authors: | Delaware, Benjamin James, Pit-Claudel, Clement F., Gross, Jason S., Chlipala, Adam |
---|---|
Other Authors: | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
Format: | Article |
Language: | en_US |
Published: |
Association for Computing Machinery
2014
|
Online Access: | http://hdl.handle.net/1721.1/91993 https://orcid.org/0000-0002-9427-4891 https://orcid.org/0000-0001-7085-9417 https://orcid.org/0000-0002-1900-3901 |
Similar Items
-
Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant
by: Delaware, Benjamin James, et al.
Published: (2021) -
Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
by: Pit-Claudel, Clément, et al.
Published: (2021) -
The end of history? Using a proof assistant to replace language design with library design
by: Chlipala, Adam, et al.
Published: (2021) -
Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
by: Pit-Claudel, Clement Francois, et al.
Published: (2021) -
The end of history? Using a proof assistant to replace language design with library design
by: Chlipala, Adam, et al.
Published: (2020)