Contact Info
Some interesting events
 Check out the Continuation calculus by Bram Geron and
me: try it or read
the
paper, which has been presented at COS and appeared in EPTCS vol 127. Also see the submitted paper A type system for Continuation Calculus.
 We have a special master
track Mathematical
Foundations of Computer Science.
 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.
 RDP 2013 , in
Eindhoven (coorganiser and PC member
of TLCA 2013)
 ITP 2013 (PC member)
 We are part of the best
computer science institute within the Netherlands, according to
the official
research assessment report.
Slides of presentations
 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 Intelligent Systems (IS) of the ICIS
(Institute for Computing and Information Science) of Radboud
University Nijmegen and head of the Foundations group of this section.
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.
Profielwerkstukken (Dutch)
We houden een lijst bij van suggesties voor
profielwerkstukken voor het VWO. Deze suggesties zijn lang niet
allemaal van mij, maar als je er vragen over hebt kun je me mailen en
zal ik proberen je verder door te verwijzen.
Research Interests
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).
I am the project leader of several research projects, most notably the ARPA project: Advancing the Real use of Proof
Assistants.
Some Professional Activities

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, Montréal,
Québec, 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 20152016 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.
 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