Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines

Yannick Forster forster@ps.uni-saarland.de, Dominique Larchey-Wendling dominique.larchey-wendling@loria.fr

This repository contains the Coq formalisation of the paper “Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines” (pre-print), currently under review.

How to compile the code

make coq should do the job. The files are tested to compile with The Coq Proof Assistant, version 8.8.2 (October 2018).

The compiled HTML version of the files can be found here or in the docs subdirectory of this repository.