Skip to content
/ fiat Public
forked from mit-plv/fiat

Mostly Automated Synthesis of Correct-by-Construction Programs

License

Notifications You must be signed in to change notification settings

bendy/fiat

 
 

Repository files navigation

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

This repository holds the source code of Fiat, a Coq ADT synthesis library.

Dependencies:

  • To build the library: Coq 8.4pl6
  • To step through the examples: GNU Emacs 24.3+, Proof General 4.4+
  • To extract and run OCaml code: OCaml 4.02.0+

Compiling and running the code

  • To build the core library: make fiat-core
  • To build the SQL-like libary: make querystructures
  • To build the parsers libary: make parsers

About

Mostly Automated Synthesis of Correct-by-Construction Programs

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages

  • Coq 87.2%
  • OCaml 10.4%
  • Assembly 1.2%
  • TeX 0.6%
  • Python 0.3%
  • Makefile 0.2%
  • Other 0.1%