From Undecidability.ILL.Bsm Require Export bsm_defs bsm_utils.
(* 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 BSM_HALTING. (* Halting problem for Minsky machines *)
(* 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 BSM_HALTING. (* Halting problem for Minsky machines *)