@inproceedings{freek2013a,
	Author = {R. Krebbers and Freek Wiedijk},
	Booktitle = {Foundations of Software Science and Computation Structures - 16th International Conference, FOSSACS 2013},
	Date-Added = {2014-11-16 23:18:17 +0000},
	Date-Modified = {2014-11-16 23:20:16 +0000},
	Editor = {Frank Pfenning},
	Pages = {257--272},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Title = {Separation Logic for Non-local Control Flow and Block Scope Variables},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/nonlocal.pdf},
	Volume = {7794},
	Year = {2013}}

@article{freek2012c,
	Author = {Freek Wiedijk},
	Date-Added = {2014-11-16 23:15:51 +0000},
	Date-Modified = {2014-11-16 23:18:03 +0000},
	Journal = {Journal of Automated Reasoning},
	Number = {1},
	Pages = {107--109},
	Title = {Review of "Handbook of Practical Logic and Automated Reasoning," by John R. Harrison, Cambridge University Press, 2009},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/review.pdf},
	Volume = {49},
	Year = {2012}}

@article{freek2012b,
	Author = {Freek Wiedijk},
	Date-Added = {2014-11-16 23:14:31 +0000},
	Date-Modified = {2014-11-16 23:15:38 +0000},
	Journal = {Logical Methods in Computer Science},
	Number = {1},
	Pages = {1--26},
	Title = {A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/miz3/miz3.pdf},
	Volume = {8},
	Year = {2012}}

@inproceedings{freek2012a,
	Author = {Freek Wiedijk},
	Booktitle = {UITP 2010, 9th International Workshop on User Interfaces for Theorem Provers},
	Date-Added = {2014-11-16 23:11:58 +0000},
	Date-Modified = {2014-11-16 23:14:10 +0000},
	Editor = {C. Sacerdoti Coen and D. Aspinall},
	Pages = {85-100},
	Series = {ENTCS},
	Title = {Pollack-inconsistency},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/rap.pdf},
	Volume = {285},
	Year = {2012}}

@proceedings{freek2011c,
	Date-Added = {2014-11-16 23:09:11 +0000},
	Date-Modified = {2014-11-16 23:11:41 +0000},
	Editor = {M. van Eekelen and Herman Geuvers and J. Schmalz and Freek Wiedijk},
	Keywords = {Edited},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Title = {Interactive Theorem Proving, Proceedings of the Second International Conference on Interactive Theorem Proving, ITP 2011, Berg en Dal, The Netherlands},
	Volume = {6898},
	Year = {2011}}

@inproceedings{freek2011b,
	Author = {R. Krebbers and Freek Wiedijk},
	Booktitle = {Intelligent Computer Mathematics, Calculemus 2011 and MKM 2011},
	Date-Added = {2014-11-16 23:07:02 +0000},
	Date-Modified = {2014-11-16 23:08:59 +0000},
	Editor = {J.H. Davenport and W.M. Farmer and F. Rabe},
	Pages = {301--303},
	Publisher = {Springer},
	Series = {Lecture Notes in Artificial Intelligence},
	Title = {A formalization of the C99 standard in HOL, isabelle and Coq},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/cicm2011.pdf},
	Volume = {6824},
	Year = {2011}}

@inproceedings{freek2011a,
	Author = {Freek Wiedijk},
	Booktitle = {Types for Proofs and Programs, TYPES 2009, Revised Selected Papers, EPTCS 53},
	Date-Added = {2014-11-16 23:05:21 +0000},
	Date-Modified = {2014-11-16 23:06:42 +0000},
	Editor = {T. Hirschowitz},
	Pages = {47--61},
	Title = {Stateless HOL},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/stateless.pdf},
	Year = {2011}}

@inproceedings{freek2010b,
	Author = {Herman Geuvers and  R. Krebbers and  J. McKinna & Freek Wiedijk},
	Booktitle = {Proceedings of the 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, EPTCS 34},
	Date-Added = {2014-11-16 23:01:35 +0000},
	Date-Modified = {2014-11-16 23:04:44 +0000},
	Editor = {K. Crary and M. Miculan},
	Pages = {53--67},
	Title = {Pure Type Systems without Explicit Contexts},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/Gi-revised-final.pdf},
	Year = {2010}}

@inproceedings{freek2010a,
	Author = {C. Tankink and Herman Geuvers and  J. McKinna and Freek Wiedijk},
	Booktitle = {Intelligent Computer Mathematics, 10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010 and 9th International Conference, MKM 2010},
	Date-Added = {2014-11-16 22:58:39 +0000},
	Date-Modified = {2014-11-16 23:01:21 +0000},
	Editor = {S. Autexier, J. Calmet and D. Delahaye and P.D.F. Ion and L. Rideau and  R. Rioboo and A.P. Sexton},
	Pages = {440--454},
	Publisher = {Springer},
	Series = {Lecture Notes in Artificial Intelligence},
	Title = {Proviola: a Tool for Proof Re-animation},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/proviola.pdf},
	Volume = {6167},
	Year = {2010}}

@article{freek2009e,
	Author = {Freek Wiedijk},
	Date-Added = {2014-11-16 22:52:52 +0000},
	Date-Modified = {2014-11-16 22:56:31 +0000},
	Journal = {Studies in Logic Grammar and Rhetoric},
	Number = {31},
	Title = {Statistics on digital libraries of mathematics},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/stats.pdf},
	Volume = {28},
	Year = {2009}}

@techreport{freek2009d,
	Author = {M. Niqui and Freek Wiedijk},
	Date-Added = {2014-11-16 22:49:55 +0000},
	Date-Modified = {2014-11-16 22:52:15 +0000},
	Institution = {University of Nijmegen},
	Number = {ICIS-R09007},
	Title = {`Many Digits' Friendly Competition},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/comp_rep.pdf},
	Year = {2009}}

@article{freek2009c,
	Author = {G. Cornelissen, W. de Graaf and W. van der Kallen and J. Sijsling and B. de Smit and J. Stevens and Freek Wiedijk},
	Date-Added = {2014-11-16 22:45:36 +0000},
	Date-Modified = {2014-11-16 22:48:11 +0000},
	Journal = {Nieuw Archief voor Wiskunde},
	Number = {3},
	Pages = {197--200},
	Title = {Wiskundig onderzoek per computer?},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/gunther.pdf},
	Volume = {5/10},
	Year = {2009}}

@article{freek2009b,
	Author = {Freek Wiedijk},
	Date-Added = {2014-11-16 22:44:11 +0000},
	Date-Modified = {2014-11-16 22:45:50 +0000},
	Journal = {Nieuwsbrief van de NVTI},
	Pages = {61--68},
	Title = {Practising logic through the web},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/nvti-proofweb.pdf},
	Volume = {13},
	Year = {2009}}

@article{freek2009a,
	Author = {Freek Wiedijk},
	Date-Added = {2014-11-16 22:40:41 +0000},
	Date-Modified = {2014-11-16 22:42:26 +0000},
	Journal = {Sadhana},
	Keywords = {formalization of mathematics, Mizar, social choice theory, Ar- row's theorem, Gibbard-Satterthwaite theorem, proof errors},
	Number = {1},
	Pages = {193--220},
	Title = {Formalizing Arrow's theorem},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/arrow.pdf},
	Volume = {34},
	Year = {2009}}

@article{freek2008e,
	Author = {Freek Wiedijk},
	Date-Added = {2014-11-16 22:38:20 +0000},
	Date-Modified = {2014-11-16 22:40:11 +0000},
	Journal = {Notices of the American Mathematical Society},
	Number = {11},
	Pages = {1408--1414},
	Title = {Formal proof--getting started},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/notices.pdf},
	Volume = {55},
	Year = {2008}}

@inproceedings{freek2008d,
	Author = {P. Corbineau and Herman Geuvers and Cezary Kaliszyk and J. McKinna and Freek Wiedijk},
	Booktitle = {Proceedings of the 3rd Semantic Wiki Workshop (SemWiki 2008) at the 5th European Semantic Web Conference (ESWC 2008)},
	Date-Added = {2014-11-16 22:35:09 +0000},
	Date-Modified = {2014-11-16 22:38:06 +0000},
	Editor = {C. Lange and  S. Schaffer and H. Skaf-Molli and M. V{\"o}lkel},
	Title = {Position paper: A real Semantic Web for mathematics deserves a real semantics},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/position-paper.pdf},
	Year = {2008}}

@techreport{freek2008c,
	Author = {Cezary Kaliszyk, Femke van Raamsdonk and Freek Wiedijk and  H. Wupper and M. Hendriks and R. de Vrijer},
	Date-Added = {2014-11-16 22:32:51 +0000},
	Date-Modified = {2014-11-16 22:34:56 +0000},
	Institution = {Radboud University Nijmegen},
	Number = {ICIS-R08016},
	Title = {Deduction using the ProofWeb system},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/proofweb-manual.pdf},
	Year = {2008}}

@inproceedings{freek2008b,
	Author = {Freek Wiedijk},
	Booktitle = {Wiskunde en profil, Het gezicht van de wiskunde, Vakantiecursus 2008},
	Date-Added = {2014-11-16 22:29:33 +0000},
	Date-Modified = {2014-11-16 22:32:26 +0000},
	Number = {Syllabus 58},
	Pages = {107--130},
	Publisher = {CWI},
	Title = {De kunst van het bewijzen},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/syllabus.pdf},
	Year = {2008}}

@proceedings{freek2008a,
	Author = {Freek Wiedijk},
	Date-Added = {2014-11-16 22:26:12 +0000},
	Date-Modified = {2014-11-16 22:29:09 +0000},
	Editor = {S. Autexier and J. Campbell and J. Rubio and V. Sorge and Masakazu Suzuki and Freek Wiedijk},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Title = {Intelligent Computer Mathematics, 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28-August 1, 2008, Proceedings},
	Volume = {5144},
	Year = {2008}}

@inproceedings{freek2007e,
	Author = {Cezary Kaliszyk and  Freek Wiedijk and  M. Hendriks and Femke van Raamsdonk},
	Booktitle = {PATE'07, International Workshop on Proof Assistants and Types in Education},
	Date-Added = {2014-11-16 22:23:06 +0000},
	Date-Modified = {2014-11-16 22:25:28 +0000},
	Editor = {Herman Geuvers & P. Courtieu},
	Pages = {37--50},
	Title = {Teaching logic using a state-of-the-art proof assistant},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/webded1.pdf},
	Year = {2007}}

@techreport{freek2007d,
	Author = {J. Carette and Freek Wiedijk (editors)},
	Date-Added = {2014-11-16 22:20:29 +0000},
	Date-Modified = {2014-11-16 22:22:28 +0000},
	Institution = {RISC-Linz},
	Keywords = {Edited},
	Number = {07-10},
	Title = {Programming Languages for Mechanized Mathematics Workshop, Informal Proceedings},
	Year = {2007}}

@inproceedings{freek2007f,
	Author = {Freek Wiedijk},
	Booktitle = {Theorem Proving in Higher Order Logics 2007},
	Date-Added = {2014-11-16 22:16:50 +0000},
	Date-Modified = {2014-11-16 22:20:04 +0000},
	Editor = {K. Schneider and J. Brandt},
	Pages = {383--399},
	Publisher = {Springer},
	Series = {Lecture Notes in Artificial Intelligence},
	Title = {Mizar's Soft Type System},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/mizar/miztype.pdf},
	Volume = {4732},
	Year = {2007}}

@inproceedings{freek2007c,
	Author = {Freek Wiedijk},
	Booktitle = {From Insight to Proof, Festschrift in Honour of Andrzej Trybulec},
	Date-Added = {2014-11-16 22:14:12 +0000},
	Date-Modified = {2014-11-16 22:16:46 +0000},
	Editor = {R. Matuszwski and A. Zalewska},
	Pages = {121--133},
	Title = {The QED Manifesto Revisited},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/qed2.pdf},
	Year = {2007}}

@inproceedings{freek2007b,
	Author = {Cezary Kaliszyk and Freek Wiedijk},
	Booktitle = { Towards Mechanized Mathematical Assistants, Calculemus 2007, Hagenberg},
	Date-Added = {2014-11-16 22:11:24 +0000},
	Date-Modified = {2014-11-16 22:13:37 +0000},
	Editor = {M. Kauers and M. Kerber and  R. Miner and W. Windsteiger},
	Publisher = {Springer},
	Series = {Lecture Notes in Artificial Intelligence},
	Title = {Certified Computer Algebra on top of an Interactive Theorem Prover},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/holcas.pdf},
	Volume = {4573},
	Year = {2007}}

@article{freek2007a,
	Author = {Herman Geuvers and M. Niqui and Bas Spitters and Freek Wiedijk},
	Date-Added = {2014-11-16 22:08:41 +0000},
	Date-Modified = {2014-11-16 22:11:04 +0000},
	Journal = {Mathematical Structures in Computer Science},
	Number = {1},
	Pages = {3--36},
	Title = {Constructive analysis, types and exact real numbers},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/editorial.pdf},
	Volume = {17},
	Year = {2007}}

@article{freek2006e,
	Author = {Freek Wiedijk},
	Date-Added = {2014-11-16 22:06:51 +0000},
	Date-Modified = {2014-11-16 22:08:13 +0000},
	Journal = {Journal of Applied Logic},
	Pages = {622--645},
	Title = {Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/zfc-etc/zfc-etc.pdf},
	Volume = {4},
	Year = {2006}}

@article{freek2006c,
	Author = {Freek Wiedijk},
	Date-Added = {2014-11-16 22:02:16 +0000},
	Date-Modified = {2014-11-16 22:03:57 +0000},
	Journal = {Nieuwsbrief van de NVTI},
	Pages = {14--23},
	Title = {On the usefulness of formal methods},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/nvti.pdf},
	Year = {2006}}

@article{freek2006a,
	Author = {Henk Barendregt and Freek Wiedijk},
	Date-Added = {2014-11-16 22:00:34 +0000},
	Date-Modified = {2014-11-16 22:02:07 +0000},
	Journal = {Euclides},
	Title = {Bewijzen: romantisch of cool},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/euclides.pdf},
	Year = {2006}}

@article{freek2005b,
	Author = {Henk Barendregt and Freek Wiedijk},
	Date-Added = {2014-11-16 21:58:07 +0000},
	Date-Modified = {2014-11-16 22:00:12 +0000},
	Journal = {Transactions A of the Royal Society},
	Number = {1835},
	Pages = {2351--2375},
	Title = {The Challenge of Computer Mathematics},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/rspaper.pdf},
	Volume = {363},
	Year = {2005}}

@article{freek2005,
	Author = {Michael Beeson and Freek Wiedijk},
	Date-Added = {2014-11-13 23:11:09 +0000},
	Date-Modified = {2014-11-16 22:29:28 +0000},
	Journal = {Journal of Symbolic Computation},
	Keywords = {Logic, Symbolic computation},
	Number = {5},
	Pages = {523--538},
	Title = {The meaning of infinity in calculus and computer algebra systems},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/limits1.pdf},
	Volume = {39},
	Year = {2005}}

@techreport{freek2004d,
	Author = {L. Cruz-Filipe and Freek Wiedijk},
	Date-Added = {2014-11-15 23:26:42 +0000},
	Date-Modified = {2014-11-15 23:28:26 +0000},
	Institution = {University of Nijmegen},
	Number = {NIII-R0431},
	Title = {Equational Reasoning in Algebraic Structures: a Complete Tactic},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/hrefl-ii.pdf},
	Year = {2004}}

@inproceedings{freek2004b,
	Author = {Herman Geuvers and Freek Wiedijk},
	Booktitle = {LFM'04, Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages, Cork, Ireland},
	Date-Added = {2014-11-15 23:19:27 +0000},
	Date-Modified = {2014-11-15 23:22:52 +0000},
	Editor = {Carsten Sch{\"u}rmann},
	Pages = {32--45},
	Title = {A logical framework with explicit conversions},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/LambdaF.pdf},
	Year = {2004}}

@proceedings{freek2004c,
	Date-Added = {2014-11-15 23:15:57 +0000},
	Date-Modified = {2014-11-15 23:18:38 +0000},
	Editor = {Freek Wiedijk},
	Keywords = {Edited},
	Number = {Report III-R0429},
	Publisher = {University of Nijmegen},
	Title = {Dutch Proof Tools Day 2004, Program + Proceedings},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/ptd2004.pdf},
	Year = {2004}}

@inproceedings{freek2004a,
	Author = {Freek Wiedijk},
	Booktitle = {Types for Proofs and Programs: Third International Workshop, TYPES 2003, Torino, Italy},
	Date-Added = {2014-11-15 23:05:26 +0000},
	Date-Modified = {2014-11-15 23:08:04 +0000},
	Editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
	Pages = {378--393},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Title = {Formal proof sketches},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/sketches2.pdf},
	Volume = {3085},
	Year = {2004}}

@techreport{freek2003d,
	Author = {M. Giero and Freek Wiedijk},
	Date-Added = {2014-11-15 23:23:46 +0000},
	Date-Modified = {2014-11-16 23:26:18 +0000},
	Institution = {University of Nijmegen},
	Number = {NIII-R0333},
	Title = {MMode, a Mizar Mode for the proof assistant Coq},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/mmode/mmode.pdf},
	Year = {2003}}

@inproceedings{freek2003b,
	Author = {Freek Wiedijk and J. Zwanenburg},
	Booktitle = {Theorem Proving in Higher Order Logics, Proceedings of TPHOLs 2003},
	Date-Added = {2014-11-15 23:10:09 +0000},
	Date-Modified = {2014-11-15 23:12:20 +0000},
	Editor = {David Basin and Burkhart Wolff},
	Pages = {221--237},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Title = {First Order Logic with Domain Conditions},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/partial.pdf},
	Volume = {2758},
	Year = {2003}}

@inproceedings{freek2003c,
	Author = {Freek Wiedijk},
	Booktitle = {th Dutch Proof Tools Day, Program + Proceedings, CWI, Amsterdam, 2003},
	Date-Added = {2014-11-15 23:01:20 +0000},
	Date-Modified = {2014-11-15 23:12:36 +0000},
	Editor = {Wan Fokkink and Jaco van de Pol},
	Title = {Formal proof sketches},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/notes/sketches.pdf},
	Year = {2003}}

@inproceedings{freek2003a,
	Author = {Freek Wiedijk},
	Booktitle = {Mathematical Knowledge Management, Proceedings of MKM 2003},
	Date-Added = {2014-11-15 22:58:28 +0000},
	Date-Modified = {2014-11-15 23:00:33 +0000},
	Editor = {Andrea Asperti and Bruno Buchberger and James Davenport},
	Pages = {188--2002},
	Title = {Comparing mathematical provers},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/comparison/diffs.pdf},
	Year = {2003}}

@proceedings{freek2002d,
	Date-Added = {2014-11-15 23:13:42 +0000},
	Date-Modified = {2014-11-15 23:15:24 +0000},
	Editor = {Herman Geuvers and Freek Wiedijk},
	Keywords = {Edited},
	Number = {2646},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Title = {Types for Proofs and Programs, International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002},
	Year = {2002}}

@article{freek2002c,
	Author = {Marcus Wenzel and Freek Wiedijk},
	Date-Added = {2014-11-15 22:45:08 +0000},
	Date-Modified = {2014-11-15 22:46:23 +0000},
	Journal = {Journal of Automated Reasoning},
	Pages = {3889--411},
	Title = {A comparison of the mathematical proof languages Mizar and Isar},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/romantic.pdf},
	Year = {2002}}

@article{freek2002b,
	Author = {Freek Wiedijk},
	Date-Added = {2014-11-15 22:41:14 +0000},
	Date-Modified = {2014-11-15 22:43:16 +0000},
	Journal = {Journal of Automated Reasoning},
	Keywords = {Automath, Formalized mathematics, Proof objects, Type theory},
	Pages = {365--387},
	Title = {A new implementation of Automath},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/aut/aut.pdf},
	Volume = {29},
	Year = {2002}}

@article{freek2002a,
	Author = {Herman Geuvers and Freek Wiedijk and J. Zwanenburg},
	Date-Added = {2014-11-15 22:31:13 +0000},
	Date-Modified = {2014-11-15 22:41:11 +0000},
	Journal = {Journal of Symbolic Computation},
	Pages = {271--286},
	Title = {A Constructive Algebraic Hierarchy in Coq},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/alghier1.pdf},
	Year = {2002}}

@inproceedings{freek2001b,
	Author = {Herman Geuvers and Freek Wiedijk and J. Zwanenburg},
	Booktitle = {Types for Proofs and Programs, Proceedings of the International Workshop, TYPES 2000, Durham},
	Date-Added = {2014-11-15 22:27:28 +0000},
	Date-Modified = {2014-11-15 22:40:00 +0000},
	Editor = {Paul Callaghan and Zhaohui Luo and James McKinna and Robert Pollack},
	Pages = {96--111},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Title = {A Constructive Proof of the Fundamental Theorem of Algebra without using the Rationals},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/kneser.pdf},
	Volume = {2277},
	Year = {2001}}

@inproceedings{freek2001a,
	Author = {Freek Wiedijk},
	Booktitle = {Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh},
	Date-Added = {2014-11-15 22:24:03 +0000},
	Date-Modified = {2014-11-15 22:26:21 +0000},
	Editor = {Richard Boulton and Paul Jackson},
	Pages = {378--393},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Title = {Mizar Light for HOL Light},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/mizar/miz.pdf},
	Volume = {2152},
	Year = {2001}}

@inproceedings{freek2000,
	Author = {Herman Geuvers and Freek Wiedijk and J. Zwanenburg},
	Booktitle = {Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon},
	Date-Added = {2014-11-15 22:18:43 +0000},
	Date-Modified = {2014-11-15 22:23:31 +0000},
	Editor = {John Harrison and Mark Aagaard},
	Pages = {162--178},
	Series = {Lecture Notes in Computer Science},
	Title = {Equational Reasoning via Partial Reflection},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/pubs/partrefl.pdf},
	Volume = {1869},
	Year = {2000}}

@phdthesis{freej1991c,
	Author = {Freek Wiedijk},
	Date-Added = {2014-11-15 22:16:19 +0000},
	Date-Modified = {2014-11-15 22:17:39 +0000},
	School = {University of Amsterdam},
	Title = {Persistence in Algebraic Specifications},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/perspect/perspect.pdf},
	Year = {1991}}

@incollection{freek1991b,
	Author = {S. Mauw and Freek Wiedijk},
	Booktitle = {Algebraic Methods II: Theory, Tools and Applications},
	Date-Added = {2014-11-15 22:14:10 +0000},
	Date-Modified = {2014-11-15 22:16:01 +0000},
	Editor = {Jan A. Bergstra and L.M.G. Feijs},
	Pages = {341--361},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Title = {Specification of the transit node in PSFd},
	Volume = {490},
	Year = {1991}}

@article{freek1991a,
	Author = {Jan A. Bergstra and S. Mauw and Freek Wiedijk},
	Date-Added = {2014-11-15 22:11:27 +0000},
	Date-Modified = {2014-11-15 22:14:08 +0000},
	Journal = {International Journal of Foundations of Computer Science},
	Number = {2},
	Pages = {43--65},
	Title = {Uniform algebraic specifications of finite sets with equality},
	Volume = {1},
	Year = {1991}}

@mastersthesis{freek1986,
	Author = {Freek Wiedijk},
	Date-Added = {2014-11-15 22:08:51 +0000},
	Date-Modified = {2014-11-15 22:11:13 +0000},
	School = {University of Amsterdam},
	Title = {Conforme supergravitatie zonder constraints},
	Url_Pdf = {http://www.cs.ru.nl/F.Wiedijk/scriptie/supergravitatie.pdf},
	Year = {1986}}

@article{freek1983,
	Author = {W. Bosma and H. Jager and Freek Wiedijk},
	Date-Added = {2014-11-15 22:07:12 +0000},
	Date-Modified = {2014-11-15 22:08:33 +0000},
	Journal = {Indagnationes Mathematica},
	Pages = {281--299},
	Title = {Some metrical observations on the approximation by continued fractions},
	Volume = {45},
	Year = {1983}}

@book{freek2006d,
	Date-Added = {2014-11-16 22:04:07 +0000},
	Date-Modified = {2014-11-16 22:06:00 +0000},
	Editor = {Freek Wiedijk},
	Foreword = {Dana S. Scott},
	Publisher = {Springer},
	Series = {Lecture Notes in Artificial Intelligence},
	Title = {The Seventeen Provers of the World},
	Volume = {3600}}