Contact Info
Some interesting events
- Check out the Continuation calculus by Bram Geron and
me: try it or read
the
paper , accepted for presentation
at COS .
- RDP 2013 , in
Eindhoven (co-organiser 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.
- 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.
Slides of presentations
- 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
- 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 Lambda-Calculus, 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 25-26, 2009, Radboud University Nijmegen,
A review of the Curry-Howard-De Bruijn formulas-as-types 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 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.
- 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 logica-informatica perspectief
Who I am & What I do
I am Professor of Computer Science (Computer Assisted Reasoning) 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 am the Director of Education for the Computer Science and Information Science curricula at Radboud
University Nijmegen. 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, 28-30 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.
-
Co-editor (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 co-chair 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,
Curry-Howard Implementation Techniques / Connecting Humans and
Type-checkers, 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,
ICALP2003-workshop MLC 2003 (co-chair), 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 (IST-1999-29001-TYPES) in Berg en Dal (near
Nijmegen), Netherlands. As part of the workshop, there was a special
afternoon celebration of the 60th birthday of Per Martin-Löf.
Look at the TYPES2002
homepage for the videos and slides of the talks of
Dana Scott, Jean-Yves Girard and Peter
Aczel. (These are the three talks given in honour of Per
Martin-Löf.)
- Former trustee of the MKM (Mathematical Knowledge Management) Interest Group (until October 2006).
Education
If you want to do a Master in Foundations of CS, look here
We also start a special master
track Mathematical
Foundations of Computer Science, together with
the Algebra and Logic
group of the Mathematics
department.
In the year 2012-2013 I am teaching the following courses
In the year 2011-2012 I am teaching the following course
In the year 2010-2011 I taught the following courses
In the year 2009-2010 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 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
- 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
- IST-FET 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