Will it Fit?

This Coq project includes:

• LambdaFit, a deeply-embedded imperative and concurrent
  lambda-calculus equipped with tracing garbage collection.
• IrisFit, an Iris-based Separation Logic
  for proving heap-space bounds of LambdaFit programs.

Setup & build

This project needs opam to install dependencies.
You can run ./setup.sh to create a local opam switch with correct
dependencies, and build the project.
Please allow at least 30 minutes for the installation and build to
run.

To manually build the project, run make or dune build.

Architecture

The architecture is as follows:

• lib/ for signed multisets and possibly null fractions.
• spacelang/ for (almost not modified) files from
  SpaceLang, taken with
  the authorization of the authors.
• language/ for the syntax & "oblivious" semantics of the
  language.
• final/ for the "main" semantics and associated results.
• program_logic/ for program logic.
• sequential/ for the emulation of the sequential mode presented
  in A High-Level Separation Logic for Heap Space under Garbage Collection.
• examples/ for various examples.

Links with Publications

We present a correspondence between this formalization and related
papers.

• For the TOPLAS paper "Will it Fit? Verifying Heap Space Bounds of
  Concurrent Programs under Garbage Collection",
  see README_toplas.md.
• For the PhD thesis of Alexandre Moine, "Formal Verification of Heap
  Space Bounds under Garbage Collection",
  see README_thesis.md.

ProofGeneral

NB: There is a hack to work with ProofGeneral.
We have a dumb src/_CoqProject which make visible the files
produced by dune.

See issue: ProofGeneral/PG#477