Herman Geuvers


Contact Info


We coordinate the (EU funded) COST Action EUTypes CA15123, the European research network on types for programming and verification. See the project home page .

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.
  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.

Slides of presentations

  1. 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.
  2. 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.
  3. Wiskunde en computers: twee revoluties, (Freek Wiedijk en Herman Geuvers) 22e Nationale Wiskundedagen 5 februari 2016, Noordwijkerhout.
  4. Inductive and Coinductive Data Types in Typed Lambda Calculus Revisited, Invited talk at the conference TLCA, July 2 2015, Warsaw Poland.
  5. In Dutch: Logica als een oefening in Formeel Denken, Openingslezing Wiskundedialoog 2015, nascholingsdag wiskunde docenten, Radboud Universiteit Nijmegen, 10 juni 2015.
  6. Dependently typed programming in Coq, Invited talk at "The Future of Programming", January 16, 2014, Delft.
  7. The Church-Scott representation of inductive and coinductive data in (typed) lambda calculus, Talk at "Types 2014", May 12-15, 2014, Paris.
  8. 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).
  9. Pure Type Systems Revisited, Invited talk at the LIX Colloquium "Theory and Application of Formal Proofs", November 5-7, 2013, Paris.
  10. 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
  11. 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
  12. Presentation Can the computer really help us to prove theorems?, Invited talk at ICT.Open 2011 Veldhoven, November 2011.
  13. Presentation Newman's Typability Algorithm, Invited talk at Computing 2011, Symposium on 75 Years of Turing Machine and Lambda-Calculus, Karlsruhe.
  14. Presentation Degrees of undecidability of in Term Rewriting, Coimbra Portugal, Conference CSL 2009, September 2009.
  15. Invited Talk: Newman's Typability Algorithm, Ecole Polytechnique, Paris, December 1, 2009.
  16. 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.
  17. 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)
  18. N.G. de Bruijn 90 jaar: symposium 5 september 2008 Voordracht Automath in historisch perspectief (pdf file van mijn slides)
  19. 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.
  20. Alfa Lernet Summer school, Uruguay 2008: Slides and Exercises
  21. 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

Who I am & What I do

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 2015-2016 I am 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