Herman Geuvers


Contact Info

Some things of interest

  1. We have a special master specialization Mathematical Foundations of Computer Science.
  2. For the second time in a row we are part of the best computer science institute within the Netherlands, according to the official research assessment report. (Top ranked both in the 2009-2014 national Research Review Computer Science and in the 2002-2008 review.)
  3. Check out the Continuation calculus by Bram Geron for his Master thesis, and me. Please read the paper, which has been presented at COS and appeared in EPTCS vol 127. Also see the other paper A type system for Continuation Calculus, EPTCS 164, Proc. 5th International Workshop on Classical Logic and Computation, Vienna, 2014.
  4. Check out our Prover system for deduction via the web. It contains a certified calculator, a platform for hosting your courses in natural deduction and a generic proof assistant interface.

Who I am & What I do

Slides of presentations

  1. Deriving derivation rules from truth tables: classically, constructively and proof reduction, talk, via zoom, in the seminar of the Logic and Semantics Group of the Tallinn University of Technology, Estonia, as part of World Logic Day January 14, 2021 . There is also a video of the talk available.
  2. Relating Apartness and Bisimulation, talk at FSA seminar, TU Eindhoven, December 2020 and talk at SWS seminar, RU Nijmegen, January 2021.
  3. Ouderdag Informatica Talk (in Dutch) "Punten en lijnen, postbodes en handelsreizigers Graaftheorie" (Een mini-inleiding graaftheorie) at the ouderdag informatica, Radboud Universiteit Nijmegen 9 februari 2019.
  4. Computer Assisted Mathematical Proofs: using the computer to verify computers , Huygens Colloquium Science Faculty, February 4, 2019, Radboud University Nijmegen
  5. Normalisation for general constructive propositional logic , joint work with Tonny Hurkens and Iris van der Giessen, talk at Types 2018, Braga Portugal, June 2018.
  6. Proof-term reductions for general forms of natural deduction , joint work with Tonny Hurkens and Iris van der Giessen, talk at TeReSe (Term Rewriting Seminar), Nijmegen, The Netherlands, May 2018.
  7. Programming with Higher Inductive Types, Herman Geuvers (joint work with Niels van der Weide, Henning Basold, Dan Frumin, Leon Gondelman), November 17, 2017, Chinese Academy of Science, Beijing.
  8. Mathematics and computers; a revolution! , Herman Geuvers (thanks to Freek Wiedijk), March 7 2017 Lustrum Symposium GEWIS, Eindhoven University of Technology
  9. Deriving natural deduction rules from truth tables (Or: How to define If-then-else as a constructive connective), talk at ICLA 2017, Kanpur India, January 2017.
  10. Computer Assisted Mathematical Proofs: Improving Automation using Machine Learning, Herman Geuvers (thanks to Freek Wiedijk, Josef Urban, Cezary Kaliszyk), November 17, 2016 Peking University, Beijing, November 18, 2016 Chinese Academy of Science, Beijing
  11. Natural deduction for propositional logic via truth tables (Joint work with Tonny Hurkens), invited talk at the Bengt Nordstrom honorary workshop, Marstrand, Sweden, April 2016.
  12. The power of lambda calculus and types, course at the 21st Estonian Winter School in Computer Science (EWSCS) Palmse, Estonia, February 28 - March 4, 2016.
  13. Wiskunde en computers: twee revoluties, (Freek Wiedijk en Herman Geuvers) 22e Nationale Wiskundedagen 5 februari 2016, Noordwijkerhout.
  14. Inductive and Coinductive Data Types in Typed Lambda Calculus Revisited, Invited talk at the conference TLCA, July 2 2015, Warsaw Poland.
  15. In Dutch: Logica als een oefening in Formeel Denken, Openingslezing Wiskundedialoog 2015, nascholingsdag wiskunde docenten, Radboud Universiteit Nijmegen, 10 juni 2015.
  16. Dependently typed programming in Coq, Invited talk at "The Future of Programming", January 16, 2014, Delft.
  17. The Church-Scott representation of inductive and coinductive data in (typed) lambda calculus, Talk at "Types 2014", May 12-15, 2014, Paris.
  18. A type system for Continuation Calculus, Talk at "Types 2014", May 12-15, 2014, Paris (joint work with Bram Geron, Wouter Geraedts, Judith van Stegeren).
  19. Pure Type Systems Revisited, Invited talk at the LIX Colloquium "Theory and Application of Formal Proofs", November 5-7, 2013, Paris.
  20. Presentation De Bruijn's ideas on the Formalization of Mathematics, Invited talk at the workshop "Foundation of Mathematics for Computer-Aided Formalization", Padova, 9-11 January 2013
  21. Presentation Representing Streams in Second Order Logic (Coinduction and Coalgebra in Second Order Logic), Talk at Seminar "Representing Streams", Lorentz Centre, Leiden Dec 14 2012
  22. Presentation Can the computer really help us to prove theorems?, Invited talk at ICT.Open 2011 Veldhoven, November 2011.
  23. Presentation Newman's Typability Algorithm, Invited talk at Computing 2011, Symposium on 75 Years of Turing Machine and Lambda-Calculus, Karlsruhe.
  24. Presentation Degrees of undecidability of in Term Rewriting, Coimbra Portugal, Conference CSL 2009, September 2009.
  25. Invited Talk: Newman's Typability Algorithm, Ecole Polytechnique, Paris, December 1, 2009.
  26. Invited talk at Mathematical Logic in the Netherlands, May 25-26, 2009, Radboud University Nijmegen, A review of the Curry-Howard-De Bruijn formulas-as-types interpretation.
  27. Dutch Model Checking Day, April 2 2009, University of Twente Verification of Hybrid Systems in Coq, joint work of H. Geuvers, A. Koprowski, D. Synek, E. van der Weegen as part of the BRICKS AFM4 project "ARPA" (Advancing the Real use of Proof Assistants)
  28. N.G. de Bruijn 90 jaar: symposium 5 september 2008 Voordracht Automath in historisch perspectief (pdf file van mijn slides)
  29. MathWiki. We have applied for an ICT-FET project for MathWiki, but this failed to get funded. Here are the slides of a talk I gave about it at the iCIS colloquium at the RU Nijmegen (April 21, 2008). See MathWiki (by Cezary Kaliszyk) for info on our MathWiki initiative.
  30. Alfa Lernet Summer school, Uruguay 2008: Slides and Exercises
  31. Slides of my talk at the "Nationale Wiskunde Dagen" (Dutch): Helden van de wiskunde, L.E.J. Brouwer. Brouwers visie vanuit een logica-informatica perspectief

Inaugural speech

On March 9 2007, I delivered my inaugural speech at the Radboud University Nijmegen (in Dutch). You can find the speech (long and short versions) and the slides here.

Research Interests

Logic in Computer Science in general. Type theory, lambda calculus, logic, theorem provers (especially interactive ones, with a bias to those based on type theory), formalizing mathematics, computer mathematics (combining proving, computing and presentation in one integrated computer environment), software verification, automata and formal languages.

I am the project leader of several research projects, most notably the ARPA project: Advancing the Real use of Proof Assistants.

Some Professional Activities


We have a special master track Mathematical Foundations of Computer Science, together with the Algebra and Logic group of the Mathematics department.

In the year 2021-2022 I teach the following courses

In the year 2020-2021 I taught the following courses In the year 2019-2020 I taught the following courses In the year 2018-2019 I taught the following courses In the year 2017-2018 I taught the following courses In the year 2016-2017 I taught the following courses In the year 2015-2016 I taught teaching the following courses In the year 2014-2015 I taught In the year 2013-2014 I taught the following courses In the year 2012-2013 I taught teaching the following courses In the year 2011-2012 I taught the following courses In the year 2010-2011 I taught the following courses In the year 2009-2010 I taught the following course
  • The Ba course Semantiek en Logica 2, SenL2. See the SenL2 page for more info. NOTE Op 26 januari 2010 is de laatste kans om dit vak te herkansen. Schrijf je in en zie hier voor verdere details.
  • The Ma course Semantics. See the Semantics page for more info.

    Here is a list of topics for students, in case you are looking for a Research project or a Bachelor/Master Thesis project.

    Here is some info on courses I taught earlier I am the contact-person for the Master Theme Foundations. A "Master theme" is a specialization for a master studies in Computer Science (after one has finished a Bachelor). If you are interested doing a master in CS within our research group (and the NIII department), follow the link above.

    I have a separate page with course material regarding Type Theory, Proof Assistants, Formalizing Mathematics etc.

    Here is a Type Checker for the Calculus of Constructions (can be used as an interactive proof assistant for higher order predicate logic), written by a student (H. van Beek) during his `stage', as a Java applet.

    Research related Links

    Some private information