Herman Geuvers

Herman

Contact Info

Some interesting events

  1. 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.
  2. We have a special master track Mathematical Foundations of Computer Science.
  3. 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.
  4. RDP 2013 , in Eindhoven (co-organiser and PC member of TLCA 2013)
  5. ITP 2013 (PC member)
  6. We are part of the best computer science institute within the Netherlands, according to the official research assessment report.

Slides of presentations

  1. The Church-Scott representation of inductive and coinductive data in (typed) lambda calculus, Talk at "Types 2014", May 12-15, 2014, Paris.
  2. A type system for Continuation Calculus, Talk at "Types 2014", May 12-15, 2014, Paris (joint work with Bram Geron, Wouter Geraedts, Judith van Stegeren).
  3. Pure Type Systems Revisited, Invited talk at the LIX Colloquium "Theory and Application of Formal Proofs", November 5-7, 2013, Paris.
  4. 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
  5. 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
  6. Presentation Can the computer really help us to prove theorems?, Invited talk at ICT.Open 2011 Veldhoven, November 2011.
  7. Presentation Newman's Typability Algorithm, Invited talk at Computing 2011, Symposium on 75 Years of Turing Machine and Lambda-Calculus, Karlsruhe.
  8. Presentation Degrees of undecidability of in Term Rewriting, Coimbra Portugal, Conference CSL 2009, September 2009.
  9. Invited Talk: Newman's Typability Algorithm, Ecole Polytechnique, Paris, December 1, 2009.
  10. 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.
  11. 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)
  12. N.G. de Bruijn 90 jaar: symposium 5 september 2008 Voordracht Automath in historisch perspectief (pdf file van mijn slides)
  13. 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.
  14. Alfa Lernet Summer school, Uruguay 2008: Slides and Exercises
  15. 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 (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


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 2014-2015 I am teaching the following courses

In the year 2013-2014 I taught the following courses In the year 2012-2013 I taught teaching the following courses In the year 2011-2012 I taught the following courses In the year 2010-2011 I taught the following courses In the year 2009-2010 I taught the following course
  • 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


    Some private information


    herman