Fiat refines declarative specifications into functional programs that can be run with good performance, and it all happens inside Coq without modifications. Our artifact includes three examples utilizing a library for specifying ADTs with SQL-like operations and automatically deriving implementations using tactics. It also includes the manual derivation of an implementation of one such ADT that automatically caches queries.

Getting started

Thanks for evaluating this artifact! Here is how to get started:

  1. Download the paper.

  2. Download the artifact: Source code tarball (~ 130kB; see the dependencies section below)

  3. Compile the source code

    $ make sources

  4. Start exploring the examples!

    The best way to get a feeling of how the library works is to step through the semi-automated refinement of the bookstore example from the paper found in examples/BookstoreSemiAutomatic.v.

    The examples folder contains three further fully-automated example refinements of ADTs with SQL-like operations:

    CacheADT/LRUCache.v demonstrates the manual derivation of the least recently used cache discussed in Section 3.1 of the paper.

    BookstoreCache.v utilizes the LRUCache derived in CacheADT/LRUCache.v to build the version of the bookstore example from Section 4.7 which caches queries using finite differencing.

Technical details



Going further

Extracting and running OCaml code

Running make repl extracts the bookstore example code and produces a repl binary in the examples/ directory, which supports the following commands:

add_book    [author title isbn]
place_order [isbn]
get_titles  [author]
num_orders  [author]
benchmark   [nb_authors nb_books nb_orders nb_titles_queries nb_orders_queries]

To replicate the results highlighted in the paper, run examples/repl, and type

benchmark 1000 10000 100000 100000 100000

Exploring the code base

Top-level directory organization

Detailed sub-directory organization:


Definitions of computations and refinement that form the core of ADT refinement.


Definition of abstract data types (ADTs).


More pleasant notations for ADTs.


Definitions of and machinery for refining ADTs from specification to implementation.


Definitions and tactics for more specialized refinements.


Definitions and tactics for notation-friendly versions of some of the specialized refinements in ADTRefinement/Refinements


Library for specifying and refining ADTs with SQL-like operations


Definitions and notations for specifying SQL-like operations on QueryStructures


Implementations of QueryStructures