Contact Info
EUTypes
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
 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.)
 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.
 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
 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
Who I am & What I do
 I am Professor of Computer Science (Theoretical Computer Science)
in the Section Software Science
(SwS) of the ICIS (Institute for Computing and Information
Science) of Radboud University Nijmegen and head of the Foundations
group of this section.

Since January 1, 2015, I am the Research Director of the research
institute ICIS at Radboud University Nijmegen.

I was the Director of Education for the Computer Science and Information Science curricula at Radboud
University Nijmegen until March 1 2013. In Dutch: "Onderwijsdirecteur van III".
 I am also one day a week (on Thursday) Professor in
the FSA
group of the Faculty of
Mathematics and Computer Science of
the Technical University
Eindhoven.
 I do research and teaching, see below. Look
here for a brief curriculum vitae.
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
 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).
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 20172018 I am 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, 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.
In the year 20132014 I taught the following courses
 The 1st year bachelor course for Artificial
Intelligence Matrix Rekenen (IPC017) (3d quarter).
 The Master
Course Semantics
and Domain Theory IMC011, Spring 2014.
 The
course Proving
with Computer Assistance at the Technical University Eindhoven
in the spring of 2014 (3d quarter).
 The Master course (first semester) Type Theory and Coq together with Freek Wiedijk (main teacher) and Robbert Krebbers.
 The 3d year bachelor course for Computer Science Semantics of Logic Programming (IBC012) (2nd quarter).

The MFOCS
Research Seminar, with lots of other teachers, Fall 2013.
In the year 20122013 I taught teaching the following courses
 The 1st year bachelor course for Science NWIMOL090 Formal
Languages, Grammars and Automata (4th quarter).
 The Master
Course Semantics
and Domain Theory IMC011, Spring 2013.
 The course Proving with Computer Assistance at the Technical University Eindhoven in the spring of 2013 (3d quarter).
In the year 20112012 I taught the following courses
In the year 20102011 I taught the following courses
In the year 20092010 I taught the following course
 The course Proving with Computer Assistance at the Technical University Eindhoven in the spring of 2010.
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 contactperson 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
 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.
 IPA
Some private information
herman