Publications
-
L. 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;
ps,
pdf,
BiBTeX
-
L. Cruz-Filipe, "Constructive Real Analysis: a Type-Theoretical
Formalization and Applications", PhD thesis, 2004;
ps.gz,
pdf,
BiBTeX
-
L. 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;
ps,
pdf,
BiBTeX
-
L. Cruz-Filipe and B. Spitters, "Program Extraction from Large Proof
Developments",
Springer-Verlag, in D. Basin and B. Wolff (eds.), Theorem
Proving in Higher Order Logics (16th International Conference,
TPHOLs2003), pages 205-220, LNCS 2758, Springer, 2003;
ps,
pdf,
BiBTeX
-
H. Geuvers, R. Pollack, F. Wiedijk & J. 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
-
H. Geuvers, R.Pollack, F. Wiedijk & J. 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
-
H. Geuvers, F. Wiedijk & J. 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
-
H. Geuvers, F. Wiedijk & J. 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
-
S. Hinderer, "Formalization d'éléments d'analyse complexe et de
topologie en Coq", Bachelor Thesis, École Normale Supérieure de Lyon,
2003;