Research of Herman Geuvers
There is a complete list of my publications.
My topics of research are
 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
Some publications with an overview nature on these topics are:
 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 lambdacalculus, Typed lambdacalculus, 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 132199.
 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, NorthHolland, Amsterdam, 1994, pp 1024.
 The Calculus of Constructions and Higher Order Logic, in The
CurryHoward isomorphism, ed. Ph. de Groote, Volume 8 of the
"Cahiers du Centre de logique" (Universit'e catholique de
Louvain), Academia, LouvainlaNeuve (Belgium),
pp. 139191. Preliminary version: The
Calculus of Constructions and Higher Order Logic
More specifically, my research interests include, but
are not restricted to, the following. You can find lists of relevant
publications for each topic there as well.
 The connection between type theory and logic, notably via the
CurryHoward(De Bruijn) embedding of formulasastypes and
proofsasterms. 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 lambdacalculi, in Types
for Proofs and Programs, Int. Workshop TYPES '93, Nijmegen, the
Netherlands, eds. H. Barendregt and T. Nipkow, Springer, LNCS 806, pp
79107.
 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, NorthHolland, Amsterdam, 1994, pp
1024.
 The Calculus of Constructions and Higher Order
Logic, in The CurryHoward isomorphism, ed. Ph. de Groote, Volume 8 of
the "Cahiers du Centre de logique" (Universit'e catholique
de Louvain), Academia, LouvainlaNeuve (Belgium),
pp. 139191. Preliminary version: The
Calculus of Constructions and Higher Order Logic
 Metatheory 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), 155189.
 The ChurchRosser
property for betaetareduction in typed lambda calculi. In
Proceedings of the seventh annual symposium on Logic in Computer
Science, Santa Cruz, Cal., IEEE, pp 453460.
 Logics and Type
systems, PhD. Thesis, University of Nijmegen, September
1993.
 With B. Werner, On
the ChurchRosser property for Expressive Type Systems and its
Consequences for their Metatheoretic Study, in Proceedings of the
Ninth Annual Symposium on Logic in Computer Science, Paris, France,
IEEE Computer Society, pp 320329.
 With F. Barbanera and M. Fern'andez, Modularity of Strong Normalization in the
lambdaalgebraiccube, in Proceedings of the Ninth Annual
Symposium on Logic in Computer Science, Paris, France, IEEE Computer
Society, pp 406415. 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 1438.
 With G. Barthe,
Modular Properties of Algebraic Type Systems,
in Higherorder algebra, Logic and Term Rewriting, Paderborn, Germany,
1995, eds. G. Dowek, J. Heering, K. Meinke, B. M"oller, Springer,
LNCS 1074, Springer, w1996, pp. 3756.
 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 183207.
 With G. Barthe,
Congruence Types, in Computer Science Logic'95
, Paderborn, Germany, 1995, ed. H. Kleine B"uhning, LNCS 1092, Springer,
1996, pp. 3651.
 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. 249264.
 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 167181.
 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!