Publications

• Evgeny Makarov and Bas Spitters The Picard Algorithm for Ordinary Differential Equations in Coq Rough Diamond in ITP2013, pdf (sources), (bib), 2013.
• Robbert Krebbers and Bas Spitters Type classes for efficient exact real arithmetic in Coq LMCS 9(1:1), 2013. 10.2168/LMCS-9(1:01)2013. PDF 1106.3448. sources (bib).
• Robbert Krebbers and Bas Spitters Computer certified efficient exact reals in Coq 1105.2751. CICM'11 LNCS 90-106, 2011. 10.1007/978-3-642-22673-1_7. PDF, bib, sources.
• Bas Spitters and Eelis van der Weegen Type Classes for Mathematics in Type Theory. Interactive theorem proving and the formalization of mathematics, Special Issue of Mathematical Structures in Computer Science, 21, 1-31, 2011 10.1017/S0960129511000119. (A shorter version `Developing the algebraic hierarchy with type classes in Coq' appeared as a Rough Diamond at ITP-10). ArXiv 1102.1323. development. bib
• Russell O'Connor and Bas Spitters A computer verified, monadic, functional implementation of the integral. Theoretical Computer Science. Volume 411, Issue 37, 7 August 2010, Pages 3386-3402 doi:10.1016/j.tcs.2010.05.031. Available at the arxiv as 0809.1552 bib
• Cezary Kaliszyk and Russell O'Connor. Computing with Classical Real Numbers. Journal of Formalized Reasoning, Vol. 2, No. 1, 2009, Pages 27--39
• Valentin Blot, Basics for algebraic numbers and a proof of Liouville’s theorem in C-CoRN PDF, 2009
• Russell O'Connor. Certified Exact Transcendental Real Number Computation in Coq. TPHOLS 2008, LNCS 5170: 246--261, Aug 2008, Proceedings
• Russell O'Connor. A Computer Verified Theory of Compact Sets. SCSS 2008, RISC-Linz Report Series 08<96>08: 148<96>162, Jul 2008, Proceedings
• Russell O'Connor. A monadic, functional implementation of real numbers. Mathematical Structures in Computer Science, Feb 2007. Volume 17, Issue 1, pp. 129--159
• Russell O'Connor. 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
• Russell O'Connor. Incompleteness & Completeness: Formalizing Logic and Analysis in Type Theory. PhD Thesis, 2009
• Luis Cruz-Filipe, Herman Geuvers, Freek Wiedijk, C-CoRN, the Constructive Coq Repository at Nijmegen MKM 2004 DOI
• Luis Cruz-Filipe, Constructive Real Analysis: a Type-Theoretical Formalization and Applications, PhD thesis, 2004; pdf, BiBTeX
• Luís Cruz-Filipe, Pierre Letouzey A Large-Scale Experiment in Executing Extracted Programs Electr. Notes Theor. Comput. Sci. 151(1): 75-91 (2006) PDF
• Luis Cruz-Filipe and Bas Spitters Program extraction from large proof developments. in Proceedings of 16th International Conference TPHOLs 2003 (in LNCS proceedings), D. Basin and B. Wolff (eds.), pages 205--220, LNCS 2758, 2003 Springer-Verlag 2003 pdf, bib.
• Luis Cruz-Filipe, A Constructive Formalization of the Fundamental Theorem of Calculus, Springer-Verlag, in H. Geuvers and F. Wiedijk (eds.), Types 2002, Proceedings of the workshop Types for Proof and Programs, pages 108-126, LNCS 2646, Springer-Verlag 2003; pdf, BiBTeX
• Sebastien Hinderer, Formalization d'éléments d'analyse complexe et de topologie en Coq, Bachelor Thesis, École Normale Supérieure de Lyon, 2003;
• Luis Cruz-Filipe, Formalizing Real Calculus in Coq, in Carreño, V., Muñoz, C. and Tahar, S. (eds.), Theorem Proving in Higher Order Logics, pages 158-166, NASA Conference Proceedings, Hampton VA, 2002; pdf, BiBTeX
• Herman Geuvers, Randy Pollack, Freek Wiedijk & Jan Zwanenburg, A Constructive Algebraic Hierarchy in Coq, in S. Linton & R. Sebasitani (eds.), Journal of Symbolic Computation, Special Issue on the Integration of Automated Reasoning and Computer Algebra Systems, 34(4), Elsevier, 271-286, 2002; ps.gz dvi
  
• Herman Geuvers, Randy Pollack, Freek Wiedijk & Jan Zwanenburg, Skeleton for the Proof development leading to the Fundamental Theorem of Algebra, Outline of the mathematics of a constructive proof of the Fundamental Theorem of Algebra
• Herman Geuvers, Freek Wiedijk & Jan Zwanenburg, A Constructive Proof of the Fundamental Theorem of Algebra without using the Rationals, in P. Callaghan, Z. Luo, J. McKinna & R. Pollack (eds.), Types for Proofs and Programs, Proceedings of the International Workshop, TYPES 2000, Durham, Springer LNCS 2277, 96-111, 2001; ps.gz dvi
• Herman Geuvers, Freek Wiedijk & Jan Zwanenburg, Equational Reasoning via Partial Reflection., in J. Harrison & M. Aagaard, Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, Springer LNCS 1869, 162-178, 2000; ps.gz dvi