Skip to content

Latest commit

 

History

History
59 lines (38 loc) · 3.57 KB

README.md

File metadata and controls

59 lines (38 loc) · 3.57 KB

Artifact for "Scaling Up Mechanized Proof Automation for Small-step Semantics"

This is the companion artifact to the paper "Scaling Up Mechanized Proof Automation for Small-step Semantics".

This artifact contains the Rocq code described in the paper.

Detailed File Description

The file CLAIMS.md links statements made in the paper with this artifact.

The file sequences.v is adapted from previous work by François Pottier, which was based on work by Xavier Leroy, with a few additions by the authors of this artifact.

File Name Spec Proof Comments Description
common.v 48 70 3 Contains common definitions and utilities used across multiple modules.
tactics.v 224 3 69 Contains custom tactics for automated proof strategies in Rcoq.
sequences.v 242 220 25 Defines operations and properties of sequences of reduction (star, plus and related lemmas).
miniml/miniml.v 650 763 70 Defines syntax and proofs for mini-ML.
miniml/miniml_ifthenelse.v 393 137 40 Defines syntax and proofs for mini-ML + if-then-else.
catala/syntax.v 521 250 9 Defines the syntax of the fragment of $\lambda^\delta$ we are dealing with.
catala/small_step.v 315 122 11 Describes the traditional small-step semantics of the language.
catala/continuations.v 452 181 35 Describes the continuation-based small-step semantics of the language.
catala/typing.v 394 90 35 Provides the typing rules and their verification for the language.
catala/simulation_cred_to_sred.v 213 219 15 Provides a simulation proof from continuation steps to small steps semantic.
catala/simulation_sred_to_cred.v 606 609 45 Provides a simulation proof from small steps to continuation steps semantic.
catala/trans.v 203 182 26 Handles the transformation that removes default terms from $\lambda^\delta$ intermediate languages.
Total 4261 2846 383

This table was computed using the coqwc utility

Hardware Dependencies

Minimal dependencies are required. The entire proof builds in 1 minute on a recent laptop.

Building and Installation

To start developing, you first need to install opam using your package manager. According to [https://opam.ocaml.org/doc/Install.html], you can run the following commands:

bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)"
opam init

Then, you can execute the following commands to install the artifact dependencies (including Rocq):

opam switch create rocq-catala 4.14.0
opam repo add coq-released https://coq.inria.fr/opam/released
eval $(opam env --switch=rocq-catala --set-switch)
opam repository add rocq-released --all-switches
opam install . --deps-only

Step-by-Step Instructions

Once you have installed the dependencies, you can use Dune to build the Rcoq development:

dune build

Then, start your favorite interactive proof interface for Rcoq.