On synthetic undecidability in coq, with an application to the entscheidungsproblem.

Yannick Forster, Dominik Kirst, Gert Smolka

Browse the full CPP paper archive.