Herman Geuvers

Herman

Contact Info

Some things of interest

  1. Seminar Synergy of Theorem Proving and Machine Learning on Wednesday December 6, 9:30-12:30.
  2. We have a special master specialization Mathematical Foundations of Computer Science.
  3. 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.)
  4. There is an interesting Cost Action related to my research: European Research Network on Formal Proofs, COST action CA20111.

Who I am & What I do

Some slides of presentations

  1. Programming with Higher Inductive Types, talk at FSA seminar, TU Eindhoven, December 2021.
  2. Proof terms for generalized classical natural deduction, talk in the Types Conference 2021 , 27th International Conference on Types for Proofs and Programs on 14 – 18 June 2021, Leiden University, the Netherlands.
  3. 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.
  4. Relating Apartness and Bisimulation, talk at FSA seminar, TU Eindhoven, December 2020 and talk at SWS seminar, RU Nijmegen, January 2021.
  5. 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.
  6. Computer Assisted Mathematical Proofs: using the computer to verify computers , Huygens Colloquium Science Faculty, February 4, 2019, Radboud University Nijmegen
  7. Normalisation for general constructive propositional logic , joint work with Tonny Hurkens and Iris van der Giessen, talk at Types 2018, Braga Portugal, June 2018.
  8. 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.
  9. 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.
  10. Mathematics and computers; a revolution! , Herman Geuvers (thanks to Freek Wiedijk), March 7 2017 Lustrum Symposium GEWIS, Eindhoven University of Technology
  11. 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.
  12. 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
  13. 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.
  14. 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.
  15. Wiskunde en computers: twee revoluties, (Freek Wiedijk en Herman Geuvers) 22e Nationale Wiskundedagen 5 februari 2016, Noordwijkerhout.
  16. Inductive and Coinductive Data Types in Typed Lambda Calculus Revisited, Invited talk at the conference TLCA, July 2 2015, Warsaw Poland.
  17. In Dutch: Logica als een oefening in Formeel Denken, Openingslezing Wiskundedialoog 2015, nascholingsdag wiskunde docenten, Radboud Universiteit Nijmegen, 10 juni 2015.
  18. Dependently typed programming in Coq, Invited talk at "The Future of Programming", January 16, 2014, Delft.
  19. The Church-Scott representation of inductive and coinductive data in (typed) lambda calculus, Talk at "Types 2014", May 12-15, 2014, Paris.
  20. 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).
  21. Pure Type Systems Revisited, Invited talk at the LIX Colloquium "Theory and Application of Formal Proofs", November 5-7, 2013, Paris.
  22. 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
  23. 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
  24. Presentation Can the computer really help us to prove theorems?, Invited talk at ICT.Open 2011 Veldhoven, November 2011.
  25. Presentation Newman's Typability Algorithm, Invited talk at Computing 2011, Symposium on 75 Years of Turing Machine and Lambda-Calculus, Karlsruhe.
  26. Presentation Degrees of undecidability of in Term Rewriting, Coimbra Portugal, Conference CSL 2009, September 2009.
  27. Invited Talk: Newman's Typability Algorithm, Ecole Polytechnique, Paris, December 1, 2009.
  28. 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.
  29. 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)
  30. N.G. de Bruijn 90 jaar: symposium 5 september 2008 Voordracht Automath in historisch perspectief (pdf file van mijn slides)
  31. 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.
  32. Alfa Lernet Summer school, Uruguay 2008: Slides and Exercises
  33. 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.

Education

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 2023-2024 I teach the following courses

In the year 2022-2023 I taught the following courses In the year 2021-2022 I taught 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

Some Professional Activities (Old)

Research related Links