A Formally Verified Abstract Account of Gdel's Incompleteness Theorems.

Andrei Popescu, Dmitriy Traytel

Browse the full CADE paper archive.