Modular Proof of Strong Normalization for the Calculus of Constructions. - Herman Geuvers; Mark-Jan Nederhof (J. Funct. Program., 1991)

The Church-Rosser Property for beta-eta-reduction in Typed lambda-Calculi - Herman Geuvers (LICS, 1992)

Conservativity between Logics and Typed lambda Calculi. - Herman Geuvers (TYPES, 1993)

Modularity of Strong Normalization and Confluence in the algebraic-lambda-Cube - Franco Barbanera; Maribel Fernández; Herman Geuvers (LICS, 1994)

On the Church-Rosser Property for Expressive Type Systems and its Consequences for their Metatheoretic Study - Herman Geuvers; Benjamin Werner (LICS, 1994)

A short and flexible proof of Strong Normalization for the Calculus of Constructions. - Herman Geuvers (TYPES, 1994)

Congruence Types. - Gilles Barthe; Herman Geuvers (CSL, 1995)

Modular Properties of Algebraic Type Systems. - Gilles Barthe; Herman Geuvers (HOA, 1995)

A Simple Model Construction for the Calculus of Constructions. - Milena Stefanova; Herman Geuvers (TYPES, 1995)

Extending Models of Second Order Predicate Logic to Models of Second Dependent Type Theory. - Herman Geuvers (CSL, 1996)

Modularity of Strong Normalization in the Algebraic-lambda-Cube. - Franco Barbanera; Maribel Fernández; Herman Geuvers (J. Funct. Program., 1997)

Safe Proof Checking in Type Theory with Y. - Herman Geuvers; Erik Poll; Jan Zwanenburg (CSL, 1999)

Some logical and syntactical observations concerning the first-order dependent type system lambda-P. - Herman Geuvers; Erik Barendsen (Math. Struct. Comput. Sci., 1999)

Explicit Substitution On the Edge of Strong Normalization. - Roel Bloo; Herman Geuvers (Theor. Comput. Sci., 1999)

Equational Reasoning via Partial Reflection. - Herman Geuvers; Freek Wiedijk; Jan Zwanenburg (TPHOLs, 2000)

Constructive Reals in Coq: Axioms and Categoricity. - Herman Geuvers; Milad Niqui (TYPES, 2000)

A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals. - Herman Geuvers; Freek Wiedijk; Jan Zwanenburg (TYPES, 2000)

Proof-Assistants Using Dependent Type Systems. - Henk Barendregt; Herman Geuvers (Handbook of Automated Reasoning, 2001)

Induction Is Not Derivable in Second Order Dependent Type Theory. - Herman Geuvers (TLCA, 2001)

Open Proofs and Open Terms: A Basis for Interactive Logic. - Herman Geuvers; Gueorgui I. Jojgov (CSL, 2002)

A Constructive Algebraic Hierarchy in Coq. - Herman Geuvers; Randy Pollack; Freek Wiedijk; Jan Zwanenburg (J. Symb. Comput., 2002)

Proof by computation in the Coq system. - Martijn Oostdijk; Herman Geuvers (Theor. Comput. Sci., 2002)

Preface. - Herman Geuvers; Fairouz Kamareddine (Mathematics, Logic and Computation @ ICALP, 2003)

A Calculus of Tactics and Its Operational Semantics. - Gueorgui I. Jojgov; Herman Geuvers (MKM Symposium, 2003)

C-CoRN, the Constructive Coq Repository at Nijmegen. - Luís Cruz-Filipe; Herman Geuvers; Freek Wiedijk (MKM, 2004)

Rewriting for Fitch Style Natural Deductions. - Herman Geuvers; Rob Nederpelt (RTA, 2004)

A Logical Framework with Explicit Conversions. - Herman Geuvers; Freek Wiedijk (LFM@IJCAR, 2004)

An Interactive Algebra Course with Formalised Proofs and Definitions. - Andrea Asperti; Herman Geuvers; Iris Loeb; Lionel Elie Mamane; Claudio Sacerdoti Coen (MKM, 2005)

From Deduction Graphs to Proof Nets: Boxes and Sharing in the Graphical Presentation of Deductions. - Herman Geuvers; Iris Loeb (MFCS, 2006)

(In)consistency of Extensions of Higher Order Logic and Type Theory. - Herman Geuvers (TYPES, 2006)

Deduction Graphs with Universal Quantification. - Herman Geuvers; Iris Loeb (TERMGRAPH@ETAPS, 2007)

Natural deduction via graphs: formal definition and computation rules. - Herman Geuvers; Iris Loeb (Math. Struct. Comput. Sci., 2007)

Constructive analysis, types and exact real numbers. - Herman Geuvers; Milad Niqui; Bas Spitters; Freek Wiedijk (Math. Struct. Comput. Sci., 2007)

Preface to the special issue: Constructive analysis, types and exact real numbers. - Bas Spitters; Herman Geuvers; Milad Niqui; Freek Wiedijk (Math. Struct. Comput. Sci., 2007)

Introduction to Type Theory. - Herman Geuvers (LerNet ALFA Summer School, 2008)

A Real Semantic Web for Mathematics Deserves a Real Semantics. - Cezary Kaliszyk; Pierre Corbineau; Freek Wiedijk; James McKinna; Herman Geuvers (SemWiki, 2008)

Preface. - S. Barry Cooper; Herman Geuvers; Anand Pillay; Jouko A. Väänänen (Ann. Pure Appl. Log., 2008)

Degrees of Undecidability in Term Rewriting. - Jörg Endrullis; Herman Geuvers; Hans Zantema (CSL, 2009)

A Logically Saturated Extension of lambdaµµ. - Lionel Elie Mamane; Herman Geuvers; James McKinna (Calculemus/MKM, 2009)

Degrees of Undecidability in Rewriting - Jörg Endrullis; Herman Geuvers; Hans Zantema (CoRR, 2009)

Social processes, program verification and all that. - Andrea Asperti; Herman Geuvers; Raja Natarajan (Math. Struct. Comput. Sci., 2009)

Proviola: A Tool for Proof Re-animation. - Carst Tankink; Herman Geuvers; James McKinna; Freek Wiedijk (AISC/MKM/Calculemus, 2010)

A Wiki for Mizar: Motivation, Considerations, and Initial Prototype. - Josef Urban; Jesse Alama; Piotr Rudnicki; Herman Geuvers (AISC/MKM/Calculemus, 2010)

Automated Machine-Checked Hybrid System Safety Proofs. - Herman Geuvers; Adam Koprowski; Dan Synek; Eelis van der Weegen (ITP, 2010)

Pure Type Systems without Explicit Contexts - Herman Geuvers; Robbert Krebbers; James McKinna; Freek Wiedijk (LFMTP, 2010)

Narrating Formal Proof (Work in Progress). - Carst Tankink; Herman Geuvers; James McKinna (UITP, 2010)

Multi-output Ranking for Automated Reasoning. - Daniel Kühlwein; Josef Urban; Evgeni Tsivtsivadze; Herman Geuvers; Tom Heskes (KDIR, 2011)

Learning2Reason. - Daniel Kühlwein; Josef Urban; Evgeni Tsivtsivadze; Herman Geuvers; Tom Heskes (Calculemus/MKM, 2011)

Semantic Graph Kernels for Automated Reasoning. - Evgeni Tsivtsivadze; Josef Urban; Herman Geuvers; Tom Heskes (SDM, 2011)

Levels of undecidability in rewriting. - Jörg Endrullis; Herman Geuvers; Jakob Grue Simonsen; Hans Zantema (Inf. Comput., 2011)

The correctness of Newman's typability algorithm and some of its extensions. - Herman Geuvers; Robbert Krebbers (Theor. Comput. Sci., 2011)

The lambda-mu-T-calculus - Herman Geuvers; Robbert Krebbers; James McKinna (CoRR, 2012)

Communicating Formal Proofs: The Case of Flyspeck. - Carst Tankink; Cezary Kaliszyk; Josef Urban; Herman Geuvers (ITP, 2013)

Explicit convertibility proofs in pure type systems. - Floris van Doorn; Herman Geuvers; Freek Wiedijk (LFMTP, 2013)

Formal Mathematics on Display: A Wiki for Flyspeck. - Carst Tankink; Cezary Kaliszyk; Josef Urban; Herman Geuvers (MKM/Calculemus/DML, 2013)

The λμT-calculus. - Herman Geuvers; Robbert Krebbers; James McKinna (Ann. Pure Appl. Log., 2013)

Continuation calculus. - Bram Geron; Herman Geuvers (COS, 2013)

Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description. - Cezary Kaliszyk; Josef Urban; Jirí Vyskocil; Herman Geuvers (CICM, 2014)

A type system for Continuation Calculus. - Herman Geuvers; Wouter Geraedts; Bram Geron; Judith van Stegeren (CL&C, 2014)

Type Theory based on Dependent Inductive and Coinductive Types. - Henning Basold; Herman Geuvers (LICS, 2016)

Deriving Natural Deduction Rules from Truth Tables. - Herman Geuvers; Tonny Hurkens (ICLA, 2017)

A Formalisation of Consistent Consequence for Boolean Equation Systems. - Myrthe van Delft; Herman Geuvers; Tim A. C. Willemse (ITP, 2017)

Proof Terms for Generalized Natural Deduction. - Herman Geuvers; Tonny Hurkens (TYPES, 2017)

Higher Inductive Types in Programming. - Henning Basold; Herman Geuvers; Niels van der Weide (J. Univers. Comput. Sci., 2017)

Finite sets in homotopy type theory. - Dan Frumin; Herman Geuvers; Léon Gondelman; Niels van der Weide (CPP, 2018)

A benchmark for C program verification. - Marko C. J. D. van Eekelen; Daniil Frumin; Herman Geuvers; Léon Gondelman; Robbert Krebbers; Marc Schoolderman; Sjaak Smetsers; Freek Verbeek; Benoît Viguier; Freek Wiedijk (CoRR, 2019)

The Construction of Set-Truncated Higher Inductive Types. - Niels van der Weide; Herman Geuvers (MFPS, 2019)

Strong Normalization for Truth Table Natural Deduction. - Herman Geuvers; Iris van der Giessen; Tonny Hurkens (Fundam. Informaticae, 2019)

Tactic Learning and Proving for the Coq Proof Assistant. - Lasse Blaauwbroek; Josef Urban; Herman Geuvers (LPAR, 2020)

The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq. - Lasse Blaauwbroek; Josef Urban; Herman Geuvers (CICM, 2020)

The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq. - Lasse Blaauwbroek; Josef Urban; Herman Geuvers (CoRR, 2020)

Relating Apartness and Bisimulation. - Herman Geuvers; Bart Jacobs 001 (Log. Methods Comput. Sci., 2021)

Apartness and Distinguishing Formulas in Hennessy-Milner Logic. - Herman Geuvers (A Journey from Process Algebra via Timed Automata to Model Learning, 2022)

Diaframe: automated verification of fine-grained concurrent programs in Iris. - Ike Mulder; Robbert Krebbers; Herman Geuvers (PLDI, 2022)

Classical Natural Deduction from Truth Tables. - Herman Geuvers; Tonny Hurkens (TYPES, 2022)

Directed branching bisimulation via apartness and positive logic. - Herman Geuvers; Anton Golov (CoRR, 2022)

Characteristics of de Bruijn's early proof checker Automath. - Herman Geuvers; Rob Nederpelt (Fundam. Informaticae, 2022)

Hashing Modulo Context-Sensitive 𝛼-Equivalence. - Lasse Blaauwbroek; Miroslav Olsák; Herman Geuvers (Proc. ACM Program. Lang., 2024)

Impredicative Encodings of Inductive and Coinductive Types. - Steven Bronsveld; Herman Geuvers; Niels van der Weide (FSCD, 2025)

Master Thesis Impredicative Encodings of Inductive and Coinductive Types. - Steven Bronsveld; Herman Geuvers; Niels van der Weide (CoRR, 2025)