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 - Universiteit Nijmegen - Home Page
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.
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 mini-inleiding graaftheorie) at the ouderdag informatica, Radboud
Universiteit Nijmegen 9 februari 2019.
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.
In Dutch: Logica als een
oefening in Formeel Denken, Openingslezing Wiskundedialoog 2015,
nascholingsdag wiskunde docenten, Radboud Universiteit Nijmegen, 10
juni 2015.
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
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)
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.
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.
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 2020-2021 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 2019-2020 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 2018-2019 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 2017-2018 I taught the following courses
The course
NWI-IPC002,
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.
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, 28-30 July 2008.
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.
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.
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).
Research related Links
The Coq homepage. Coq is a proof assistant based on type theory.
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.