Contact Info
Some things of interest

Seminar Synergy of Theorem Proving and Machine Learning on Wednesday December 6, 9:3012:30.
 We have a special master
specialization Mathematical
Foundations of Computer Science.
 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 20092014
national Research Review Computer Science and in the 20022008 review.)
 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
 Programming with Higher Inductive Types, talk at FSA seminar,
TU Eindhoven, December 2021.
 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.
 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.
 Relating Apartness and
Bisimulation, talk at FSA seminar,
TU Eindhoven, December 2020
and talk at SWS seminar, RU
Nijmegen, January 2021.
 Ouderdag Informatica Talk (in
Dutch) "Punten en lijnen, postbodes en handelsreizigers Graaftheorie"
(Een miniinleiding graaftheorie) at the ouderdag informatica, Radboud
Universiteit Nijmegen 9 februari 2019.
 Computer Assisted Mathematical Proofs: using
the computer to verify computers , Huygens Colloquium
Science Faculty,
February 4, 2019,
Radboud University Nijmegen
 Normalisation for general
constructive propositional logic , joint work with Tonny Hurkens
and Iris van der Giessen, talk at Types 2018, Braga Portugal, June
2018.
 Proofterm 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.
 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.
 Mathematics and computers; a
revolution! , Herman Geuvers (thanks to Freek Wiedijk), March 7
2017 Lustrum Symposium GEWIS, Eindhoven University of Technology
 Deriving natural deduction
rules from truth tables (Or: How to define Ifthenelse as a
constructive connective), talk at ICLA 2017, Kanpur India, January
2017.
 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
 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.
 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.
 Wiskunde en computers: twee
revoluties, (Freek Wiedijk en Herman Geuvers) 22e Nationale
Wiskundedagen 5 februari 2016, Noordwijkerhout.
 Inductive and Coinductive Data Types
in Typed Lambda Calculus Revisited, Invited talk at the
conference TLCA, July 2 2015, Warsaw Poland.
 In Dutch: Logica als een
oefening in Formeel Denken, Openingslezing Wiskundedialoog 2015,
nascholingsdag wiskunde docenten, Radboud Universiteit Nijmegen, 10
juni 2015.
 Dependently typed programming in
Coq, Invited talk at "The Future of Programming", January 16, 2014, Delft.
 The ChurchScott
representation of inductive and coinductive data in (typed) lambda
calculus, Talk at "Types 2014", May 1215, 2014, Paris.
 A type system for
Continuation Calculus, Talk at "Types 2014", May 1215, 2014,
Paris (joint work with Bram Geron, Wouter Geraedts, Judith van
Stegeren).
 Pure Type Systems Revisited,
Invited talk at the LIX Colloquium "Theory and Application of Formal
Proofs", November 57, 2013, Paris.
 Presentation De Bruijn's ideas on the
Formalization of Mathematics, Invited talk at the workshop "Foundation of Mathematics
for ComputerAided Formalization", Padova, 911 January 2013
 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
 Presentation Can the computer really help
us to prove theorems?, Invited talk at ICT.Open 2011 Veldhoven,
November 2011.
 Presentation Newman's Typability
Algorithm, Invited talk at Computing 2011, Symposium on 75 Years
of Turing Machine and LambdaCalculus, Karlsruhe.
 Presentation Degrees of undecidability
of in Term Rewriting, Coimbra Portugal, Conference CSL 2009,
September 2009.
 Invited Talk: Newman's Typability Algorithm, Ecole Polytechnique, Paris, December 1, 2009.
 Invited talk at Mathematical Logic in the Netherlands, May 2526, 2009, Radboud University Nijmegen,
A review of the CurryHowardDe Bruijn formulasastypes interpretation.
 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)
 N.G. de Bruijn 90 jaar:
symposium 5 september 2008
Voordracht Automath in historisch perspectief (pdf file van mijn slides)
 MathWiki. We have applied for an ICTFET 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.
 Alfa Lernet Summer school, Uruguay 2008: Slides and Exercises
 Slides of my talk at the "Nationale Wiskunde Dagen" (Dutch): Helden van de wiskunde, L.E.J. Brouwer.
Brouwers visie vanuit een logicainformatica 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 20232024 I teach the following courses
In the year 20222023 I taught the following courses

The MFOCS
Research Seminar, with lots of other teachers, Fall
2022.
 The Master
course Type
Theory and Coq, first semester, together with Freek Wiedijk
(main teacher).
 The course
Proving with Computer Assistance at the Technical
University Eindhoven in the spring of 2023 (3d quarter).
 The Bachelor
course Complexity,
IBC028, 4th quarter.
In the year 20212022 I taught the following courses
 The Master course
Semantics and Domain Theory IMC011, Fall 2021.

The MFOCS
Research Seminar, with lots of other teachers, Fall
2021.
 The Master
course Type
Theory and Coq, first semester, together with Freek Wiedijk
(main teacher).
 The course
Proving with Computer Assistance at the Technical
University Eindhoven in the spring of 2022 (3d quarter).
In the year 20202021 I taught the following courses
 The MFOCS Research Seminar, with lots of other
teachers, Fall 2020.
 The Master
course Type
Theory and Coq, first semester, together with Freek Wiedijk
(main teacher).
 The
course
Proving with Computer Assistance at the Technical University
Eindhoven in the spring of 2021 (3d quarter).
 The Bachelor
course Complexity,
IBC028, 4th quarter.
In the year 20192020 I taught the following courses

The MFOCS
Research Seminar, with lots of other teachers, Fall 2019.
 The Master course Semantics and Domain Theory IMC011, Fall 2019.
 The Master course
Type Theory and
Coq, second semester, together with Freek Wiedijk (main
teacher).
 The Bachelor
course Complexity
IBC028, 3d quarter, together with Hans Zantema.
 The course Proving with Computer Assistance at the
Technical University Eindhoven in the spring of 2020 (3d quarter).
In the year 20182019 I taught the following courses

The MFOCS
Research Seminar, with lots of other teachers, Fall 2018.
 The Master course Type Theory and Coq, second semester, together with Freek Wiedijk (main teacher).
 The
course
Proving
with Computer Assistance at the Technical University Eindhoven
in the spring of 2019 (3d quarter).
In the year 20172018 I taught the following courses
 The course
NWIIPC002,
Talen en Automaten (Formal Languages and Automata), in the 2nd quarter
for 1st year bachelor students Computer Science, but only teh first lecture.

The MFOCS
Research Seminar, with lots of other teachers, Fall 2017.
 The Master course
Semantics and Domain Theory IMC011, Spring 2018.
 The Master course Type Theory and Coq, second semester, together with Freek Wiedijk (main teacher).
 The course Proving with Computer Assistance at the
Technical University Eindhoven in the spring of 2018 (3d quarter).
In the year 20162017 I taught the following courses
 The course
NWIIPC002,
Talen en Automaten (Formal Languages and Automata), in the 2nd quarter
for 1st year bachelor students Computer Science.
 The Master course Type Theory and Coq, second semester, together with Freek Wiedijk (main teacher).

The MFOCS
Research Seminar, with lots of other teachers, Fall 2016.
 The Master course
Semantics and Domain Theory IMC011, Spring 2017.
 The
course
Proving
with Computer Assistance at the Technical University Eindhoven
in the spring of 2017 (3d quarter).
In the year 20152016 I taught teaching the following courses
 The course
NWIIPC002, Talen
en Automaten (Formal Languages and Automata), in the 2nd quarter
for 1st year bachelor students Computer Science.
 The Huygens College
NWIHC001, Reflection:
a powerful and ubiquitous logical mechanism, in the 2nd quarter.
 (Jointly with Aleks Kissinger) The course
NWIIPC017, Matrix
Rekenen , in the 3d quarter for 1st year bachelor students
Computer Science.
 The Master course Type Theory and Coq, second semester, together with Freek Wiedijk (main teacher).

The MFOCS
Research Seminar, with lots of other teachers, Spring 2016.
 The Master course
Semantics
and Domain Theory
Semantics and Domain Theory IMC011, Spring 2016.
 The
course Proving with Computer Assistance at the Technical University Eindhoven
in the spring of 2016 (3d quarter).
In the year 20142015 I taught
 The
course
Matrix Rekenen (IPC017) (3d quarter) for 1st year bachelor students
Computer Science.
 The
course
Matrix Rekenen (1st quarter) for 2nd year bachelor
Computer Science and 1st year bachelor Artificial Intelligence.
 The 1st year bachelor course for Science NWIMOL090
Formal
Languages, Grammars and Automata, (2nd quarter).
 The Master course (first semester) Type Theory and Coq together with Freek Wiedijk (main teacher) and Robbert Krebbers.

The MFOCS
Research Seminar, with lots of other teachers, Fall 2014.
 The Master
Course
Semantics
and Domain Theory
Semantics and Domain Theory IMC011, Spring 2015.
 The
course Proving
with Computer Assistance at the Technical University Eindhoven
in the spring of 2015 (3d quarter).
 The 3d year bachelor course for Computer
Science
Semantics of Logic Programming (IBC012) has been phased out, but
I will organise one exam in 20142015.
Some Professional Activities (Old)
 RDP 2013 , in
Eindhoven (coorganiser and PC member
of TLCA 2013)
 ITP 2013 (PC member)

Programme Committee member
of FOSSACS 2010

Programme Committee member
of LICS 2010

Programme Committee member
of SemWiki 2009

Programme Committee member
of Calculemus 2009
 Invited Speaker at MLNL'09

Programme Committee member
of UITP'08
8th International Workshop On User Interfaces for Theorem Provers
(TPHOLS'08 Satellite Workshop Friday, 22nd August 2008, Montreal,
Quebec, Canada)

Programme Committee member
of MKM08 7th
International Conference on Mathematical Knowledge Management MKM 2008
Birmingham, UK, 2830 July 2008.
 Invited Speaker at International Summer School on
Language Engineering and Rigorous Software Development
February 25 to March 1, 2008
Piriapolis, Uruguay

Coorganiser of the Symposium Reflections on Type Theory, Lambda Calculus, and the Mind,
celebrating Henk Barendregt's 60th birthday. Monday 17 December 2007, Radboud University Nijmegen, The Netherlands.

Coeditor (together with E. Barendsen, V. Capretta and M. Niqui) of the Book Reflections on Type Theory, Lambda Calculus, and the Mind,
Essays Dedicated to Henk Barendregt on the Occasion of his 60th Birthday, Radboud University Nijmegen, The Netherlands.

Coorganiser and program cochair of the PATE workshop,
an RDP07 associated
workshop, June 2007, Paris. The procedings are now available online.

Coorganiser of the MAP
2007 meeting, which was held in Leiden (Netherlands) from
January 8th until January 12th, 2007.

Coorganiser of the small TYPES workshop CHIT CHAT,
CurryHoward Implementation Techniques / Connecting Humans and
Typecheckers, December 2006.
 Organisation chair and PC member of the Logic Colloquium 2006, which we
organise under auspices of the ASL
 I am also editor in chief of the proceedings of LC2006 which will appear
in the
Lectures Notes on Logic LNL series.
 Invited Speaker at the International Symposium on Mathematical Foundations of
Computer Science

Member of the Steering Committee of the EU Coordination Action Types.
 Programme Committee member of TYPES Summer School 2002,
ICALP2003workshop MLC 2003 (cochair), MKM 2003, MKM 2004, FLOPS
2004, TLCA 2005, TYPES Summer School 2005, CLAC 2006, HOR 2007.
 Member of the BCI (committee for the
evaluation of research proposals in Computer Science of NWO, the Dutch national science
foundation), 2001  2004.

Coorganiser of the small TYPES workshop Constructive analysis,
types and exact real numbers October 2005. The proceedings of this
workshop has appeared as MSCS Volume 17, Issue 01, 2007.

Coorganiser of the small TYPES workshop Types for Mathematics /
Libraries of Formal Mathematics November 2004.
 Organiser of the 2002 Workshop of the EC TYPES
Network of Excellence (IST199929001TYPES) in Berg en Dal (near
Nijmegen), Netherlands. As part of the workshop, there was a special
afternoon celebration of the 60th birthday of Per MartinLöf.
Look at the TYPES2002
homepage for the videos and slides of the talks of
Dana Scott, JeanYves Girard and Peter
Aczel. (These are the three talks given in honour of Per
MartinLöf.)
 Former trustee of the MKM (Mathematical Knowledge Management) Interest Group (until October 2006).
Research related Links
 The Coq homepage. Coq is a proof assistant based on type theory.
 Mathematical Knowledge Management Interest Group: MKM
 EU Coordination Action Types
 Calculemus Project, Systems for Integrated Computation and Deduction Calculemus
 ISTFET project  Mowgli
Mathematics On the Web, Get it by Logic and Interfaces
 Mathematical Knowledge Management Network MKMNet
 MAP,Mathematics,
Algorithms, Proofs. The MAP group intends to gather people with
connected topics of interest, such as constructive algebra, computer
algebra, designers and users of proof systems.
herman