Research of Herman Geuvers

• Type theory: type systems, typed (and untyped) lambda calculus, its connection with logic and (interactive) theorem proving.
• Formalizing Mathematics: interactive theorem proving, systems for representing mathematics, doing and studying (large) formalizations
• Computer Mathematics: integrating the mathematical activities of defining, proving and computing into a system that also supports the presentation of the mathematical content

• Logics and Type systems, PhD. Thesis, University of Nijmegen, September 1993.
• With H. Barendregt, Proof Assistants using Dependent Type Systems, chapter of the Handbook of Automated Reasoning, eds. A. Robinson and A. Voronkov, Elsevier 2001.
• With R.P. Nederpelt, Untyped lambda-calculus, Typed lambda-calculus, sections 32 and 33 in Logic: Mathematics, Language, Computer Science and Philosophy, Volume II, H.C.M. de Swart et al., Peter Lang, Frankfurt am Main, 1994, pp 132--199.
• Edited together with R.P. Nederpelt and R.C. de Vrijer, Selected Papers on Automath, Volume 133 in Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1994, pp 1024.
• The Calculus of Constructions and Higher Order Logic, in The Curry-Howard isomorphism, ed. Ph. de Groote, Volume 8 of the "Cahiers du Centre de logique" (Universit'e catholique de Louvain), Academia, Louvain-la-Neuve (Belgium), pp. 139-191. Preliminary version: The Calculus of Constructions and Higher Order Logic

• The connection between type theory and logic, notably via the Curry-Howard(-De Bruijn) embedding of formulas-as-types and proofs-as-terms. Publications of my hand (some in cooperation with others) on this topic are
  • Logics and Type systems, PhD. Thesis, University of Nijmegen, September 1993.
  • Conservativity between logics and typed lambda-calculi, in Types for Proofs and Programs, Int. Workshop TYPES '93, Nijmegen, the Netherlands, eds. H. Barendregt and T. Nipkow, Springer, LNCS 806, pp 79-107.
  • Edited together with R.P. Nederpelt and R.C. de Vrijer, Selected Papers on Automath, Volume 133 in Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1994, pp 1024.
  • The Calculus of Constructions and Higher Order Logic, in The Curry-Howard isomorphism, ed. Ph. de Groote, Volume 8 of the "Cahiers du Centre de logique" (Universit'e catholique de Louvain), Academia, Louvain-la-Neuve (Belgium), pp. 139-191. Preliminary version: The Calculus of Constructions and Higher Order Logic
• Meta-theory of typed lambda calculi (and extensions thereof), like strong normalization, confluence and so. Publications of my hand (some in cooperation with others) on this topic are
  • With M.J. Nederhof, A modular proof of Strong Normalization for the Calculus of Constructions, Journal of Functional Programming 1, 2 (1991), 155--189.
  • The Church-Rosser property for beta-eta-reduction in typed lambda calculi. In Proceedings of the seventh annual symposium on Logic in Computer Science, Santa Cruz, Cal., IEEE, pp 453-460.
  • Logics and Type systems, PhD. Thesis, University of Nijmegen, September 1993.
  • With B. Werner, On the Church-Rosser property for Expressive Type Systems and its Consequences for their Meta-theoretic Study, in Proceedings of the Ninth Annual Symposium on Logic in Computer Science, Paris, France, IEEE Computer Society, pp 320--329.
  • With F. Barbanera and M. Fern'andez, Modularity of Strong Normalization in the lambda-algebraic-cube, in Proceedings of the Ninth Annual Symposium on Logic in Computer Science, Paris, France, IEEE Computer Society, pp 406--415. An extended version has appeared in the J. of Functional Programming, vol ... pp....
  • A short and flexible proof of Strong Normalization for the Calculus of Constructions in Types for Proofs and Programs, Int. Workshop TYPES '94, Bastad, Sweden, eds. P. Dybjer, B. Nordstr"om and J. Smith, Springer, LNCS 996, pp 14--38.
  • With G. Barthe, Modular Properties of Algebraic Type Systems, in Higher-order algebra, Logic and Term Rewriting, Paderborn, Germany, 1995, eds. G. Dowek, J. Heering, K. Meinke, B. M"oller, Springer, LNCS 1074, Springer, w1996, pp. 37--56.
• Formalizing mathematics, especially in theorem provers based on type theory. In the FTA project in Nijmegen, we have formalized a constructive proof of the Fundamental Theorem of Algebra in Coq. This joint work with Freek Wiedijk, Jan Zwanenburg, Randy Pollack, Milad Niqui and Henk Barendregt. Some interesting aspects of formalizing mathematics are: how to choose your primitives, how abstract do you work, how to present a formalized proof, how to put 'intelligence' into the theorem prover, ... Some papers:
  • Skeleton of the FTA proof
  • Partial Reflection
  • FTA proof without rationals
  • Construction of the reals in Coq
• Inductive and recursive types. I have only one paper on this (about (co)induction and (co)recursion in polymorphic lambda calculus), which only appeared in an informal proceedings. Congruence types are a way of taking a quotient over an algebraic data type in Coq (to form, e.g. the integers out of zero, succ and pred).
  • Inductive and Coinductive Types with Iteration and Recursion , in the informal proceedings of the 1992 workshop on Types for Proofs and Programs, Bastad 1992, Sweden, eds. B. Nordstrom, K. Petersson and G. Plotkin, pp 183--207.
  • With G. Barthe, Congruence Types, in Computer Science Logic'95 , Paderborn, Germany, 1995, ed. H. Kleine B"uhning, LNCS 1092, Springer, 1996, pp. 36--51.
• Models for type theories. As a matter of fact, I have only used models to prove things about the syntax, so no general abstract (categorical) models here! One paper uses models to show that some types are not inhabited in the Calculus of Constructions and another to show that types are not inhabited in second order dependent type theory.
  • With M. Stefanova, A Simple Model Construction for the Calculus of Constructions in Types for Proofs and Programs, Int. Workshop TYPES '95, Torino, Italy, eds. S. Berardi and M. Coppo, Springer, LNCS 1158, 1996, pp. 249--264.
  • Extending Models of Second Order Predicate Logic to Models of Second Order Dependent Type Theory, in Computer Science Logic, Annual Conference of the EACSL, Utrecht, September 1996, eds. D. van Dalen and M. Bezem, LNCS 1258, 1997, pp 167--181.
  • TLCA paper
• Explicit substitution. This interest grew out of considering, together with Roel Bloo, the preservation of strong normalization property (if M is SN w.r.t. beta, is M then also SN w.r.t. xbeta?) We have a general proof of this result, using recursive path ordering, for many calculi xbeta. The nice thing is that our technique allows to apply rpo to a calculus with variable binding (not a first order TRS). Actually, this whole thing grew out of trying to prove that WN implies SN for a large class of type lambda calculi (preferably containing all Pure Type Systems), which is still an open problem!
  • With R. Bloo, Explicit Substitution: on the Edge of Strong Normalization, to appear in Theoretical Computer Science.