A Mechanised Proof of the Time Invariance Thesis for the Weak Call-by-value λ-Calculus

This repository contains the code of the paper "A Mechanised Proof of the Time Invariance Thesis for the Weak Call-by-value λ-Calculus" by Yannick Forster, Fabian Kunze, Gert Smolka, and Maxi Wuttke.

A summary of the main results can be found in summary.v.

Note that this repository is a fork of the Coq Library of Undecidability Proofs, to which we contribute our results.

Installation Instructions

You need opam 2 on your system.

You need Coq 8.12.1 built on OCAML >= 4.07.1, the Smpl package, the Equations package, and the MetaCoq package for Coq. If you are using opam 2 you can use the following commands to install the dependencies on a new switch:

opam switch create coq-invariance-thesis 4.07.1+flambda
eval $(opam env)
opam repo add coq-released https://coq.inria.fr/opam/released
opam install . --deps-only

Building the project

• make all builds the library
• make summary.vo compiles only the file theories/summary.v and its dependencies
• make html generates clickable coqdoc .html in the website subdirectory
• make clean removes all build files in theories and .html files in the website directory

Compiled interfaces

The library is compatible with Coq's compiled interfaces (vos) for quick infrastructural access.

• make vos builds compiled interfaces for the library
• make vok checks correctness of the library

Troubleshooting

Windows

If you use Visual Studio Code on Windows 10 with Windows Subsystem for Linux (WSL), then local opam switches may cause issues. To avoid this, you can use a non-local opam switch, i.e. opam switch create 4.07.1+flambda.

Coq version

Be careful that this branch only compiles under Coq 8.12.1.