[isabelle] finally published online: GÃdelâs Incompleteness Theorems
A Mechanised Proof of GÃdelâs Incompleteness Theorems Using Nominal Isabelle
ââ The Isabelle formalisation uses two separate treatments of variable binding: the nominal packageâ and de Bruijn indices â . Critical details of the Isabelle proof are described, in particular gaps and errors found in the literature."
Now available online at SpringerLink:
Paywalled, but full texts available here: http://www.cl.cam.ac.uk/~lp15/papers/Formath/
This archive was generated by a fusion of
Pipermail (Mailman edition) and