Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Herman Geuvers - Home Page

Herman Geuvers

Herman

Contact Info

Who I am & What I do

I am Professor in and head of the Foundations Group of the ICIS (Institute for Computing and Information Science) of the Radboud University Nijmegen.
I also 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

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.

Detailed description of my research interests
A list of publications.
A list of projects .
A list of PhD students I supervised in some way.

Some Professional Activities

Coorganiser and program co-chair of the PATE workshop, an RDP07 associated workshop, June 2007, Paris.
Coorganiser of the MAP 2007 meeting, which will be held in Leiden (Netherlands) from January 8th through 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 inn 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.
Trustee of the MKM (Mathematical Knowledge Management) Interest Group (until October 2006).
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 will appear as an MSCS volume.
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.)

Education

In the year 2006-2007 I teach the following courses

MRI master class logic: Type Theory and Proof Assistants

Research Lab 1, 2 and 3

Engelbert Hubbers

Research:Research and Development 1 (together with Engelbert Hubbers), RenD1. See the R&D; page of Engelbert Hubbers for more info.
Semantiek en Logica 2 (together with Erik Barendsen), SenL2. See the SenL2 page of Erik for more info. For the "logic" part: here are two old exams: tentamen 2005-2006 and hertentamen 2005-2006.
Semantiek en Logica 1 in Spring 2007 (together with Engelbert Hubbers), SenL2. See the SenL1 page for more info.

Here is a list of topics for students, in case you are looking for a Research Lab project or a Thesis project.

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. <!-- <LI>ProTaGoNist, the Proof-Tools Group Netherlands.
IPA

Some private information

herman