Mostly Automated Synthesis of Correct-by-Construction Programs
Clone or download
Pull request Compare This branch is even with mit-plv:master.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
Overview
etc
src
.gitattributes
.gitignore
.gitmodules
.mailmap
.travis.yml
LICENSE
Makefile
README.md
TODO
_CoqProject.in
autogen.sh
tarball.sh
todos.sh

README.md

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