nLab Russell O'Connor

Selected writings

A formal proof of the Gödel incompleteness theorem in Coq:

On constructive analysis (with real number) in type theory implemented in Coq via the completion monad:

Understanding well-behaved lenses (in computer science) as coalgebras of the costate comonad:

category: people

Last revised on January 28, 2023 at 15:17:37. See the history of this page for a list of all contributions to it.