@article{Wiedijk02,
  title = {A New Implementation of Automath},
  author = {Freek Wiedijk},
  year = {2002},
  researchr = {https://researchr.org/publication/Wiedijk02},
  cites = {0},
  citedby = {0},
  journal = {Journal of Automated Reasoning},
  volume = {29},
  number = {3-4},
  pages = {365-387},
}

@inproceedings{MauwW89,
  title = {Specification of the Transit Node in PSF::d::},
  author = {Sjouke Mauw and Freek Wiedijk},
  year = {1989},
  researchr = {https://researchr.org/publication/MauwW89},
  cites = {0},
  citedby = {0},
  pages = {341-361},
  booktitle = {Algebraic Methods II: Theory, Tools and Applications [papers from a workshop in Mierlo, The Netherlands, September 1989]},
  editor = {Jan A. Bergstra and Loe M. G. Feijs},
  volume = {490},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-53912-3},
}

@inproceedings{GeuversWZ00,
  title = {A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals},
  author = {Herman Geuvers and Freek Wiedijk and Jan Zwanenburg},
  year = {2000},
  url = {http://link.springer.de/link/service/series/0558/bibs/2277/22770096.htm},
  tags = { algebra},
  researchr = {https://researchr.org/publication/GeuversWZ00},
  cites = {0},
  citedby = {0},
  pages = {96-111},
  booktitle = {Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000, Selected Papers},
  editor = {Paul Callaghan and Zhaohui Luo and James McKinna and Robert Pollack},
  volume = {2277},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-43287-6},
}

@inproceedings{TankinkGMW10,
  title = {Proviola: A Tool for Proof Re-animation},
  author = {Carst Tankink and Herman Geuvers and James McKinna and Freek Wiedijk},
  year = {2010},
  doi = {10.1007/978-3-642-14128-7_37},
  url = {http://dx.doi.org/10.1007/978-3-642-14128-7_37},
  researchr = {https://researchr.org/publication/TankinkGMW10},
  cites = {0},
  citedby = {0},
  pages = {440-454},
  booktitle = {Intelligent Computer Mathematics, 10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010, Paris, France, July 5-10, 2010. Proceedings},
  editor = {Serge Autexier and Jacques Calmet and David Delahaye and Patrick D. F. Ion and Laurence Rideau and Renaud Rioboo and Alan P. Sexton},
  volume = {6167},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-14127-0},
}

@inproceedings{KaliszykCWMG08,
  title = {A Real Semantic Web for Mathematics Deserves a Real Semantics},
  author = {Cezary Kaliszyk and Pierre Corbineau and Freek Wiedijk and James McKinna and Herman Geuvers},
  year = {2008},
  url = {http://ceur-ws.org/Vol-360/paper-16.pdf},
  tags = {semantics, semantic web},
  researchr = {https://researchr.org/publication/KaliszykCWMG08},
  cites = {0},
  citedby = {0},
  booktitle = {Proceedings of the 3rd Semantic Wiki Workshop (SemWiki 2008) at the 5th European Semantic Web Conference (ESWC 2008), Tenerife, Spain, June 2nd, 2008},
  editor = {Christoph Lange 0002 and Sebastian Schaffert and Hala Skaf-Molli and Max Völkel},
  volume = {360},
  series = {CEUR Workshop Proceedings},
  publisher = {CEUR-WS.org},
}

@article{GeuversW08,
  title = {A Logical Framework with Explicit Conversions},
  author = {Herman Geuvers and Freek Wiedijk},
  year = {2008},
  doi = {10.1016/j.entcs.2007.11.011},
  url = {http://dx.doi.org/10.1016/j.entcs.2007.11.011},
  researchr = {https://researchr.org/publication/GeuversW08},
  cites = {0},
  citedby = {0},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {199},
  pages = {33-47},
}

@inproceedings{BeesonW02,
  title = {The Meaning of Infinity in Calculus and Computer Algebra Systems},
  author = {Michael Beeson and Freek Wiedijk},
  year = {2002},
  url = {http://link.springer.de/link/service/series/0558/bibs/2385/23850246.htm},
  tags = { algebra},
  researchr = {https://researchr.org/publication/BeesonW02},
  cites = {0},
  citedby = {0},
  pages = {246-258},
  booktitle = {Artificial Intelligence, Automated Reasoning, and Symbolic Computation, Joint International Conferences, AISC 2002 and Calculemus 2002, Marseille, France, July 1-5, 2002, Proceedings},
  editor = {Jacques Calmet and Belaid Benhamou and Olga Caprotti and Laurent Henocque and Volker Sorge},
  volume = {2385},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-43865-3},
}

@article{SpittersGNW07,
  title = {Preface to the special issue: Constructive analysis, types and exact real numbers},
  author = {Bas Spitters and Herman Geuvers and Milad Niqui and Freek Wiedijk},
  year = {2007},
  doi = {10.1017/S0960129506005846},
  url = {http://dx.doi.org/10.1017/S0960129506005846},
  tags = {analysis},
  researchr = {https://researchr.org/publication/SpittersGNW07},
  cites = {0},
  citedby = {0},
  journal = {Mathematical Structures in Computer Science},
  volume = {17},
  number = {1},
  pages = {1},
}

@inproceedings{GeuversWZ00:0,
  title = {Equational Reasoning via Partial Reflection},
  author = {Herman Geuvers and Freek Wiedijk and Jan Zwanenburg},
  year = {2000},
  tags = {reflection},
  researchr = {https://researchr.org/publication/GeuversWZ00%3A0},
  cites = {0},
  citedby = {0},
  pages = {162-178},
  booktitle = {Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings},
  editor = {Mark Aagaard and John Harrison},
  volume = {1869},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-67863-8},
}

@article{GeuversPWZ02,
  title = {A Constructive Algebraic Hierarchy in Coq},
  author = {Herman Geuvers and Randy Pollack and Freek Wiedijk and Jan Zwanenburg},
  year = {2002},
  doi = {10.1006/jsco.2002.0552},
  url = {http://dx.doi.org/10.1006/jsco.2002.0552},
  tags = { algebra},
  researchr = {https://researchr.org/publication/GeuversPWZ02},
  cites = {0},
  citedby = {0},
  journal = {Journal of Symbolic Computation},
  volume = {34},
  number = {4},
  pages = {271-286},
}

@article{Wiedijk06,
  title = {Is ZF a hack?: Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics},
  author = {Freek Wiedijk},
  year = {2006},
  doi = {10.1016/j.jal.2005.10.011},
  url = {http://dx.doi.org/10.1016/j.jal.2005.10.011},
  researchr = {https://researchr.org/publication/Wiedijk06},
  cites = {0},
  citedby = {0},
  journal = {J. Applied Logic},
  volume = {4},
  number = {4},
  pages = {622-645},
}

@article{CaretteWW10,
  title = {Preface},
  author = {Jacques Carette and Makarius Wenzel and Freek Wiedijk},
  year = {2010},
  doi = {10.1007/s10817-009-9141-x},
  url = {http://dx.doi.org/10.1007/s10817-009-9141-x},
  researchr = {https://researchr.org/publication/CaretteWW10},
  cites = {0},
  citedby = {0},
  journal = {Journal of Automated Reasoning},
  volume = {44},
  number = {1-2},
  pages = {1-2},
}

@inproceedings{Cruz-FilipeGW04,
  title = {C-CoRN, the Constructive Coq Repository at Nijmegen},
  author = {Luís Cruz-Filipe and Herman Geuvers and Freek Wiedijk},
  year = {2004},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3119&spage=88},
  tags = {C++},
  researchr = {https://researchr.org/publication/Cruz-FilipeGW04},
  cites = {0},
  citedby = {0},
  pages = {88-103},
  booktitle = {Mathematical Knowledge Management, Third International Conference, MKM 2004, Bialowieza, Poland, September 19-21, 2004, Proceedings},
  editor = {Andrea Asperti and Grzegorz Bancerek and Andrzej Trybulec},
  volume = {3119},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-23029-7},
}

@article{BeesonW05,
  title = {The meaning of infinity in calculus and computer algebra systems},
  author = {Michael Beeson and Freek Wiedijk},
  year = {2005},
  doi = {10.1016/j.jsc.2004.12.002},
  url = {http://dx.doi.org/10.1016/j.jsc.2004.12.002},
  tags = { algebra},
  researchr = {https://researchr.org/publication/BeesonW05},
  cites = {0},
  citedby = {0},
  journal = {Journal of Symbolic Computation},
  volume = {39},
  number = {5},
  pages = {523-538},
}

@inproceedings{Cruz-FilipeW04,
  title = {Hierarchical Reflection},
  author = {Luís Cruz-Filipe and Freek Wiedijk},
  year = {2004},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3223&spage=66},
  tags = {reflection},
  researchr = {https://researchr.org/publication/Cruz-FilipeW04},
  cites = {0},
  citedby = {0},
  pages = {66-81},
  booktitle = {Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings},
  editor = {Konrad Slind and Annette Bunker and Ganesh Gopalakrishnan},
  volume = {3223},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-23017-3},
}

@inproceedings{Wiedijk03,
  title = {Comparing Mathematical Provers},
  author = {Freek Wiedijk},
  year = {2003},
  url = {http://link.springer.de/link/service/series/0558/bibs/2594/25940188.htm},
  researchr = {https://researchr.org/publication/Wiedijk03},
  cites = {0},
  citedby = {0},
  pages = {188-202},
  booktitle = {Mathematical Knowledge Management, Second International Conference, MKM 2003, Bertinoro, Italy, February 16-18, 2003, Proceedings},
  volume = {2594},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-00568-4},
}

@inproceedings{Wiedijk01,
  title = {Mizar Light for HOL Light},
  author = {Freek Wiedijk},
  year = {2001},
  url = {http://link.springer.de/link/service/series/0558/bibs/2152/21520378.htm},
  researchr = {https://researchr.org/publication/Wiedijk01},
  cites = {0},
  citedby = {0},
  pages = {378-394},
  booktitle = {Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings},
  editor = {Richard J. Boulton and Paul B. Jackson},
  volume = {2152},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-42525-X},
}

@inproceedings{KaliszykW08,
  title = {Merging Procedural and Declarative Proof},
  author = {Cezary Kaliszyk and Freek Wiedijk},
  year = {2008},
  doi = {10.1007/978-3-642-02444-3_13},
  url = {http://dx.doi.org/10.1007/978-3-642-02444-3_13},
  researchr = {https://researchr.org/publication/KaliszykW08},
  cites = {0},
  citedby = {0},
  pages = {203-219},
  booktitle = {Types for Proofs and Programs, International Conference, TYPES 2008, Torino, Italy, March 26-29, 2008, Revised Selected Papers},
  editor = {Stefano Berardi and Ferruccio Damiani and Ugo de Liguoro},
  volume = {5497},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-02443-6},
}

@article{WenzelW02,
  title = {A Comparison of Mizar and Isar},
  author = {Markus Wenzel and Freek Wiedijk},
  year = {2002},
  researchr = {https://researchr.org/publication/WenzelW02},
  cites = {0},
  citedby = {0},
  journal = {Journal of Automated Reasoning},
  volume = {29},
  number = {3-4},
  pages = {389-411},
}

@inproceedings{Wiedijk07,
  title = {Mizar s Soft Type System},
  author = {Freek Wiedijk},
  year = {2007},
  doi = {10.1007/978-3-540-74591-4_28},
  url = {http://dx.doi.org/10.1007/978-3-540-74591-4_28},
  tags = {type system},
  researchr = {https://researchr.org/publication/Wiedijk07},
  cites = {0},
  citedby = {0},
  pages = {383-399},
  booktitle = {Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings},
  editor = {Klaus Schneider and Jens Brandt},
  volume = {4732},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-540-74590-7},
}

@article{GeuversNSW07,
  title = {Constructive analysis, types and exact real numbers},
  author = {Herman Geuvers and Milad Niqui and Bas Spitters and Freek Wiedijk},
  year = {2007},
  doi = {10.1017/S0960129506005834},
  url = {http://dx.doi.org/10.1017/S0960129506005834},
  tags = {analysis},
  researchr = {https://researchr.org/publication/GeuversNSW07},
  cites = {0},
  citedby = {0},
  journal = {Mathematical Structures in Computer Science},
  volume = {17},
  number = {1},
  pages = {3-36},
}

@inproceedings{WiedijkZ03,
  title = {First Order Logic with Domain Conditions},
  author = {Freek Wiedijk and Jan Zwanenburg},
  year = {2003},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2758&spage=221},
  tags = {logic},
  researchr = {https://researchr.org/publication/WiedijkZ03},
  cites = {0},
  citedby = {0},
  pages = {221-237},
  booktitle = {Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings},
  editor = {David A. Basin and Burkhart Wolff},
  volume = {2758},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-40664-6},
}

@article{BergstraMW91,
  title = {Uniform Algebraic Specifications of Finite Sets with Equality},
  author = {Jan A. Bergstra and Sjouke Mauw and Freek Wiedijk},
  year = {1991},
  tags = {algebraic specification,  algebra},
  researchr = {https://researchr.org/publication/BergstraMW91},
  cites = {0},
  citedby = {0},
  journal = {Int. J. Found. Comput. Sci.},
  volume = {2},
  number = {1},
  pages = {43-65},
}

@inproceedings{KaliszykW07,
  title = {Certified Computer Algebra on Top of an Interactive Theorem Prover},
  author = {Cezary Kaliszyk and Freek Wiedijk},
  year = {2007},
  doi = {10.1007/978-3-540-73086-6_8},
  url = {http://dx.doi.org/10.1007/978-3-540-73086-6_8},
  tags = { algebra},
  researchr = {https://researchr.org/publication/KaliszykW07},
  cites = {0},
  citedby = {0},
  pages = {94-105},
  booktitle = {Towards Mechanized Mathematical Assistants, 14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, Hagenberg, Austria, June 27-30, 2007, Proceedings},
  editor = {Manuel Kauers and Manfred Kerber and Robert Miner and Wolfgang Windsteiger},
  volume = {4573},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-540-73083-5},
}

@inproceedings{Wiedijk03:0,
  title = {Formal Proof Sketches},
  author = {Freek Wiedijk},
  year = {2003},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3085&spage=378},
  researchr = {https://researchr.org/publication/Wiedijk03%3A0},
  cites = {0},
  citedby = {0},
  pages = {378-393},
  booktitle = {Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers},
  editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
  volume = {3085},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-22164-6},
}

@inproceedings{Wiedijk06:0,
  title = {Introduction},
  author = {Freek Wiedijk},
  year = {2006},
  doi = {10.1007/11542384_1},
  url = {http://dx.doi.org/10.1007/11542384_1},
  researchr = {https://researchr.org/publication/Wiedijk06%3A0},
  cites = {0},
  citedby = {0},
  pages = {1-9},
  booktitle = {The Seventeen Provers of the World, Foreword by Dana S. Scott},
  editor = {Freek Wiedijk},
  volume = {3600},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-30704-4},
}
@proceedings{aisc:2008,
  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},
  year = {2008},
  researchr = {https://researchr.org/publication/aisc%3A2008},
  cites = {0},
  citedby = {0},
  booktitle = {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},
  conference = {AISC},
  editor = {Serge Autexier and John Campbell and Julio Rubio and Volker Sorge and Masakazu Suzuki and Freek Wiedijk},
  volume = {5144},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-540-85109-7},
}

@proceedings{tphol:2006provers,
  title = {The Seventeen Provers of the World, Foreword by Dana S. Scott},
  year = {2006},
  researchr = {https://researchr.org/publication/tphol%3A2006provers},
  cites = {0},
  citedby = {0},
  booktitle = {The Seventeen Provers of the World, Foreword by Dana S. Scott},
  conference = {tphol},
  editor = {Freek Wiedijk},
  volume = {3600},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-30704-4},
}

@proceedings{types:2002,
  title = {Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers},
  year = {2003},
  researchr = {https://researchr.org/publication/types%3A2002},
  cites = {0},
  citedby = {0},
  booktitle = {Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers},
  conference = {TYPES},
  editor = {Herman Geuvers and Freek Wiedijk},
  volume = {2646},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-14031-X},
}