Fiat
Overview
Fiat is a library for the Coq proof assistant for synthesizing efficient correct-by-construction programs from declarative specifications. Programming by Fiat starts with a high-level description of a program, which can be written using libraries of specification languages for describing common programming tasks like querying a relational database. These specifications are then iteratively refined into efficient implementations via automated tactics. Each derivation in Fiat produces a formal proof trail certifying that the synthesized program meets the original specification. Code synthesized by Fiat can be extracted to an equivalent OCaml program that can be compiled and run as normal.
Download
| Release | Description |
|---|---|
|
2014-10-31 (Coq 8.4pl2) source • VM • VM (no GUI) |
Submission to POPL 2015 Artifact Evaluation Committee (README) |
Publications
Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant
Benjamin Delaware, Clément Pit--Claudel, Jason Gross, Adam Chlipala
Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'15). January 2015.
Deriving efficient OCaml implementations of abstract data types, from declarative specifications, in Coq, mostly automatically. The main case study works with SQL-style relational queries and insert operations.