MM.v

From Undecidability.ILL.Mm Require Export mm_defs mm_utils.

(* The halting problem for Minsky 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 MM_HALTING. (* Halting problem for Minsky machines *)