Undecidability proofs in Coq ATM - Acceptance problem HALT - Halting problem ETM - Empty language problem EQTM - Turing machine equivalence problem Rice - Rice's theorem