Russell O'Connor
Address
Location
Room N/A
Institute for Computing and Information Science
Faculty of Science, Mathematics and Computing Science
Toernooiveld,
Nijmegen, NL
Phone: +31.24.36.52249 Fax: +31.24.36.52728
Mailing
Faculty of Science, Mathematics and Computing Science
Radboud University Nijmegen,
P.O. Box 9010,
6500 GL Nijmegen
The Netherlands
Biography
Degrees
BMath in Pure Mathematics and Computer Science from the University of Waterloo, Waterloo, Ontario, Canada.
Education
2000-2003 in the Logic and Methodology of Science program at the University of California at Berkerley, California, USA.
2005-Present in the Foundations Group in the computer science deparment at Radboud University, Nijmegen, The Netherlands.
Publications
Certified Exact Transcendental Real Number Computation in Coq. TPHOLS 2008, LNCS 5170: 246-261, Aug 2008, Proceedings
A Computer Verified Theory of Compact Sets. SCSS 2008, RISCLinz Report Series 0808: 148-162, Jul 2008, Proceedings
A monadic, functional implementation of real numbers. Mathematical Structures in Computer Science, Feb 2007. Volume 17, Issue 1, pp. 129 - 159
Assembly: Circular Programming with Recursive do. The Monad.Reader, vol. 6, Jan 2007, pp. 35-53.
Essential Incompleteness of Arithmetic Verified by Coq. Theorem Proving in Higher Order Logics: 18th International Conference, TPHOLS 2005, Lecture Notes in Computer Science, Volume 3603, Aug 2005. Proceedings, pp. 245 - 260
Presentations
Formal Mathematics using Dependent Type Theory, Pure Math Club. University of Waterloo. 2009-02-25
Efficient Provably Correct Infinite Precision Real Arithmetic & More: A Monadic Approach, TPHOLs 2008. 2008-08-21
Math is Functional Programming: Implementing Real Numbers (Takahashi method), Functioneel Programmeren dag 2008. 2008-01-11
Functional Programming Imperative, Vrije Universiteit: Principles of Programming Languages. 2007-12-14
Correct Effective Real Arithmetic: A Monadic Approach, Universität Trier: Forschungsseminar Theoretische Informatik. 2007-10-04
Learning Coq by Proving Gödel's Incompleteness Theorem, Microsoft Research-INRIA Joint Centre Seminar. 2007-02-13
Implementing Analysis, MAP workshop 2007. 2007-01-08
A Monadic Approach to Certified Exact Real Arithmetic, DIAMANT/EIDMA symposium 2006. 2006-11-30
A Monadic Approach to Certified Exact Real Arithmetic, Workshop on Numbers and Proofs. 2006-06-13
Verifying the incompleteness theorems in the Coq proof assistant, ASL 2006 Annual Meeting. 2006-05-19
New Horizons of Proof: Software Verification of Gödel’s Second Incompleteness Theorem, Horizons of Truth: Gödel Centenary 2006. 2006-04-27
Few Digits: A Monadic Approach to Exact Real Arithmetic, Types 2006. 2006-04-19
Essential Incompleteness of Arithmetic Verified by Coq, DIAMANT/EIDMA symposium 2005. 2005-11-18
Essential Incompleteness of Arithmetic Verified by Coq, NIII Colloquium 2005. 2005-11-07
An Approch to Fast Real Arithmetic in Coq, Small TYPES workshop: Constructive analysis, Types and Exact Real Numbers. 2005-10-04
Essential Incompleteness of Arithmetic Verified by Coq, TPHOLs 2005. 2005-08-25