From Undecidability.ILL.Ll Require Export ill eill.

(* The halting problem for binary stack machines *)

(* Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines. Yannick Forster and Dominique Larchey-Wendling. CPP '19. http://uds-psl.github.io/ill-undecidability/ *)

About EILL_PROVABILITY.  (* Provability for elementary linear logic *)
About ILL_PROVABILITY.   (* Provability for linear logic *)
