| 2025 | FSCD | Impredicative Encodings of Inductive and Coinductive Types. | Steven Bronsveld, Herman Geuvers, Niels van der Weide |
| 2022 | PLDI | Diaframe: automated verification of fine-grained concurrent programs in Iris. | Ike Mulder, Robbert Krebbers, Herman Geuvers |
| 2020 | LPAR | Tactic Learning and Proving for the Coq Proof Assistant. | Lasse Blaauwbroek, Josef Urban, Herman Geuvers |
| 2018 | CPP | Finite sets in homotopy type theory. | Dan Frumin, Herman Geuvers, Lon Gondelman, Niels van der Weide |
| 2017 | ITP | A Formalisation of Consistent Consequence for Boolean Equation Systems. | Myrthe van Delft, Herman Geuvers, Tim A. C. Willemse |
| 2016 | LICS | Type Theory based on Dependent Inductive and Coinductive Types. | Henning Basold, Herman Geuvers |
| 2013 | ITP | Communicating Formal Proofs: The Case of Flyspeck. | Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers |
| 2011 | IC3K | Multi-output Ranking for Automated Reasoning. | Daniel Khlwein, Josef Urban, Evgeni Tsivtsivadze, Herman Geuvers, Tom Heskes |
| 2011 | SDM | Semantic Graph Kernels for Automated Reasoning. | Evgeni Tsivtsivadze, Josef Urban, Herman Geuvers, Tom Heskes |
| 2010 | AISC | Proviola: A Tool for Proof Re-animation. | Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk |
| 2010 | AISC | A Wiki for Mizar: Motivation, Considerations, and Initial Prototype. | Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers |
| 2010 | ITP | Automated Machine-Checked Hybrid System Safety Proofs. | Herman Geuvers, Adam Koprowski, Dan Synek, Eelis van der Weegen |
| 2009 | CSL | Degrees of Undecidability in Term Rewriting. | Jrg Endrullis, Herman Geuvers, Hans Zantema |
| 2006 | MFCS | From Deduction Graphs to Proof Nets: Boxes and Sharing in the Graphical Presentation of Deductions. | Herman Geuvers, Iris Loeb |
| 2002 | CSL | Open Proofs and Open Terms: A Basis for Interactive Logic. | Herman Geuvers, Gueorgui I. Jojgov |
| 1999 | CSL | Safe Proof Checking in Type Theory with Y. | Herman Geuvers, Erik Poll, Jan Zwanenburg |
| 1996 | CSL | Extending Models of Second Order Predicate Logic to Models of Second Dependent Type Theory. | Herman Geuvers |
| 1995 | CSL | Congruence Types. | Gilles Barthe, Herman Geuvers |
| 1994 | LICS | Modularity of Strong Normalization and Confluence in the algebraic-lambda-Cube | Franco Barbanera, Maribel Fernndez, Herman Geuvers |
| 1994 | LICS | On the Church-Rosser Property for Expressive Type Systems and its Consequences for their Metatheoretic Study | Herman Geuvers, Benjamin Werner |
| 1992 | LICS | The Church-Rosser Property for beta-eta-reduction in Typed lambda-Calculi | Herman Geuvers |