This repo contains the formalisation work accompanying the ESOP'26 paper "In Cantor Space No One Can Hear You Stream".
The formalization is based on a previous work by Adjej et al (Martin-Löf à la Coq, CPP'24), which itself follows a similar Agda formalization (described in Decidability of conversion for Type Theory in Type Theory, 2018). In order to avoid some work on the syntax, this project uses the AutoSubst project to generate syntax-related boilerplate.
- Install opam through your favourite means.
- Double-check that no Coq-related environment variables like COQBIN or COQPATH are set.
- Launch the following commands in the folder of this development.
opam switch create . --empty
eval $(opam env)
opam install ocaml-base-compiler=4.14.2
opam repo --this-switch add coq-released https://coq.inria.fr/opam/released
opam install . --deps-only
make
The coqdocjs subfolder is not part of this development, but an independent project vendored here for simplicity of the build process. The upstream repository can be found at https://github.com/coq-community/coqdocjs/.
The project builds on Coq version 8.19.2, see the opam file for complete dependencies. Since they are not available as opam packages, coqdocjs is simply included.
Once the dependencies have been installed, you can simply issue make in the root folder. The development should build within 10 minutes (around 3 minutes on a modern laptop).
Apart from a few harmless warnings, and the output of some examples, the build reports on the assumptions of our main theorems, using Print Assumptions.
For simplicity, the html documentation built using coqdoc is included in the artefact. It can be built again by invoking make coqdoc.
The development, rendered using the coqdoc utility, can be then browsed (as html files).