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.

References in zbMATH (referenced in 14 articles , 1 standard article )

Showing results 1 to 14 of 14.
Sorted by year (citations)

  1. Darais, David; Van Horn, David: Constructive Galois connections (2019)
  2. Drămnesc, Isabela; Jebelean, Tudor; Stratulat, Sorin: Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques (2019)
  3. Lammich, Peter: Refinement to imperative HOL (2019)
  4. Lammich, Peter; Lochbihler, Andreas: Automatic refinement to efficient data structures: a comparison of two approaches (2019)
  5. Benzaken, V.; Contejean, É.; Keller, Ch.; Martins, E.: A Coq formalisation of SQL’s execution engines (2018)
  6. Dagand, Pierre-Évariste; Tabareau, Nicolas; Tanter, Éric: Foundations of dependent interoperability (2018)
  7. Kumar, Ramana; Mullen, Eric; Tatlock, Zachary; Myreen, Magnus O.: Software verification with ITPs should use binary code extraction to reduce the TCB (short paper) (2018)
  8. Lochbihler, Andreas: Fast machine words in Isabelle/HOL (2018)
  9. Lochbihler, Andreas; Schneider, Joshua: Relational parametricity and quotient preservation for modular (co)datatypes (2018)
  10. Guéneau, Armaël; Myreen, Magnus O.; Kumar, Ramana; Norrish, Michael: Verified characteristic formulae for CakeML (2017)
  11. Blot, Arthur; Dagand, Pierre-Évariste; Lawall, Julia: From sets to bits in Coq (2016)
  12. Drămnesc, Isabela; Jebelean, Tudor; Stratulat, Sorin: Proof-based synthesis of sorting algorithms for trees (2016)
  13. Malecha, Gregory; Bengtson, Jesper: Extensible and efficient automation through reflective tactics (2016)
  14. Delaware, Benjamin; Pit-Claudel, Clément; Gross, Jason; Chlipala, Adam: Fiat: deductive synthesis of abstract data types in a proof assistant (2015)