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 *)
(* 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 *)