Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant

Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant

Show other versions (1)

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...

Full description

Bibliographic Details
Main Authors: Delaware, Benjamin James, Pit-Claudel, Clément, 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 2021
Online Access:https://hdl.handle.net/1721.1/91993.2
https://orcid.org/0000-0002-9427-4891
https://orcid.org/0000-0001-7085-9417
https://orcid.org/0000-0002-1900-3901

Internet

https://hdl.handle.net/1721.1/91993.2
https://orcid.org/0000-0002-9427-4891
https://orcid.org/0000-0001-7085-9417
https://orcid.org/0000-0002-1900-3901

Similar Items