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

Internet

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