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:
Russell O'Connor, A Monadic, Functional Implementation of Real Numbers, Math. Struc. Comp. Sci. 17 1 (2007) 129-159 [arXiv:cs/0605058, doi:10.1017/S0960129506005871]
Russell O'Connor, Certified exact transcendental real number computation in Coq, in Theorem Proving in Higher Order Logics. TPHOLs 2008, Lecture Notes in Computer Science 5170 (2008) 246-261 [arXiv:0805.2438, doi:10.1007/978-3-540-71067-7_21]
Russell O'Connor, Incompleteness and Completeness: Formalizing Logic and Analysis in Type Theory, PhD thesis, Radboud University Nijmegen (2009) [ubn:2066/76032, author webpage]
Understanding well-behaved lenses (in computer science) as coalgebras of the costate comonad:
Russell O’Connor, Lenses Are Exactly the Coalgebras for the Store Comonad (30th Nov 2010) [r6research:23705]
Russell O'Connor, Functor is to Lens as Applicative is to Biplate: Introducing Multiplate, contribution to ICFP ‘11: ACM SIGPLAN International Conference on Functional Programming (2011) [arXiv:1103.2841]
Last revised on January 28, 2023 at 15:17:37. See the history of this page for a list of all contributions to it.