Herman Geuvers

Publication Activity (10 Years)

Years Active: 1991-2024
Publications (10 Years): 24

Top Topics

Natural Deduction

Top Venues

Fundam. Informaticae

Publications

Lasse Blaauwbroek, Miroslav Olsák, Herman Geuvers
Hashing Modulo Context-Sensitive α-Equivalence. CoRR (2024)
Lasse Blaauwbroek, Miroslav Olsák, Herman Geuvers
Hashing Modulo Context-Sensitive 𝛼-Equivalence. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Herman Geuvers, Rob Nederpelt
Characteristics of de Bruijn's early proof checker Automath. CoRR (2022)
Herman Geuvers, Anton Golov
Directed branching bisimulation via apartness and positive logic. CoRR (2022)
Herman Geuvers, Tonny Hurkens
Classical Natural Deduction from Truth Tables. TYPES (2022)
Herman Geuvers, Rob Nederpelt
Characteristics of de Bruijn's early proof checker Automath. Fundam. Informaticae 185 (4) (2022)
Herman Geuvers
Apartness and Distinguishing Formulas in Hennessy-Milner Logic. A Journey from Process Algebra via Timed Automata to Model Learning (2022)
Ike Mulder, Robbert Krebbers, Herman Geuvers
Diaframe: automated verification of fine-grained concurrent programs in Iris. PLDI (2022)
Herman Geuvers, Bart Jacobs
Relating Apartness and Bisimulation. Log. Methods Comput. Sci. 17 (3) (2021)
Herman Geuvers, Bart Jacobs
Relating Apartness and Bisimulation. CoRR (2020)
Lasse Blaauwbroek, Josef Urban, Herman Geuvers
The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq. CoRR (2020)
Lasse Blaauwbroek, Josef Urban, Herman Geuvers
Tactic Learning and Proving for the Coq Proof Assistant. CoRR (2020)
Lasse Blaauwbroek, Josef Urban, Herman Geuvers
Tactic Learning and Proving for the Coq Proof Assistant. LPAR (2020)
Lasse Blaauwbroek, Josef Urban, Herman Geuvers
The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq. CICM (2020)
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
A benchmark for C program verification. CoRR (2019)
Herman Geuvers, Iris van der Giessen, Tonny Hurkens
Strong Normalization for Truth Table Natural Deduction. Fundam. Informaticae 170 (1-3) (2019)
Niels van der Weide, Herman Geuvers
The Construction of Set-Truncated Higher Inductive Types. MFPS (2019)
Dan Frumin, Herman Geuvers, Léon Gondelman, Niels van der Weide
Finite sets in homotopy type theory. CPP (2018)
Henning Basold, Herman Geuvers, Niels van der Weide
Higher Inductive Types in Programming. J. Univers. Comput. Sci. 23 (1) (2017)
Herman Geuvers, Tonny Hurkens
Proof Terms for Generalized Natural Deduction. TYPES (2017)
Herman Geuvers, Tonny Hurkens
Deriving Natural Deduction Rules from Truth Tables. ICLA (2017)
Myrthe van Delft, Herman Geuvers, Tim A. C. Willemse
A Formalisation of Consistent Consequence for Boolean Equation Systems. ITP (2017)
Henning Basold, Herman Geuvers
Type Theory based on Dependent Inductive and Coinductive Types. LICS (2016)
Henning Basold, Herman Geuvers
Type Theory based on Dependent Inductive and Coinductive Types. CoRR (2016)
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil, Herman Geuvers
Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Description. CoRR (2014)
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil, Herman Geuvers
Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description. CICM (2014)
Herman Geuvers, Wouter Geraedts, Bram Geron, Judith van Stegeren
A type system for Continuation Calculus. CL&C (2014)
Floris van Doorn, Herman Geuvers, Freek Wiedijk
Explicit convertibility proofs in pure type systems. LFMTP (2013)
Herman Geuvers, Robbert Krebbers, James McKinna
-calculus. Ann. Pure Appl. Log. 164 (6) (2013)
Bram Geron, Herman Geuvers
Continuation calculus. COS (2013)
Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers
Formal Mathematics on Display: A Wiki for Flyspeck. MKM/Calculemus/DML (2013)
Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers
Communicating Formal Proofs: The Case of Flyspeck. ITP (2013)
Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers
Formal Mathematics on Display: A Wiki for Flyspeck CoRR (2013)
Herman Geuvers, Robbert Krebbers, James McKinna
The lambda-mu-T-calculus CoRR (2012)
Carst Tankink, Herman Geuvers, James McKinna
Narrating Formal Proof (Work in Progress). Electron. Notes Theor. Comput. Sci. 285 (2012)
Daniel Kühlwein, Josef Urban, Evgeni Tsivtsivadze, Herman Geuvers, Tom Heskes
Multi-output Ranking for Automated Reasoning. KDIR (2011)
Evgeni Tsivtsivadze, Josef Urban, Herman Geuvers, Tom Heskes
Semantic Graph Kernels for Automated Reasoning. SDM (2011)
Jörg Endrullis, Herman Geuvers, Jakob Grue Simonsen, Hans Zantema
Levels of undecidability in rewriting. Inf. Comput. 209 (2) (2011)
Daniel Kühlwein, Josef Urban, Evgeni Tsivtsivadze, Herman Geuvers, Tom Heskes
Learning2Reason. Calculemus/MKM (2011)
Herman Geuvers, Robbert Krebbers
The correctness of Newman's typability algorithm and some of its extensions. Theor. Comput. Sci. 412 (28) (2011)
Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk
Proviola: A Tool for Proof Re-animation. AISC/MKM/Calculemus (2010)
Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers
A Wiki for Mizar: Motivation, Considerations, and Initial Prototype CoRR (2010)
Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk
Proviola: A Tool for Proof Re-animation CoRR (2010)
Herman Geuvers, Adam Koprowski, Dan Synek, Eelis van der Weegen
Automated Machine-Checked Hybrid System Safety Proofs. ITP (2010)
Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk
Pure Type Systems without Explicit Contexts LFMTP (2010)
Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers
A Wiki for Mizar: Motivation, Considerations, and Initial Prototype. AISC/MKM/Calculemus (2010)
Jörg Endrullis, Herman Geuvers, Hans Zantema
Degrees of Undecidability in Rewriting CoRR (2009)
Andrea Asperti, Herman Geuvers, Raja Natarajan
Social processes, program verification and all that. Math. Struct. Comput. Sci. 19 (5) (2009)
Lionel Elie Mamane, Herman Geuvers, James McKinna
A Logically Saturated Extension of lambdaµµ. Calculemus/MKM (2009)
Jörg Endrullis, Herman Geuvers, Hans Zantema
Degrees of Undecidability in Term Rewriting. CSL (2009)
Herman Geuvers, Freek Wiedijk
A Logical Framework with Explicit Conversions. Electron. Notes Theor. Comput. Sci. 199 (2008)
Herman Geuvers, Iris Loeb
Deduction Graphs with Universal Quantification. Electron. Notes Theor. Comput. Sci. 203 (1) (2008)
Herman Geuvers
Introduction to Type Theory. LerNet ALFA Summer School (2008)
Cezary Kaliszyk, Pierre Corbineau, Freek Wiedijk, James McKinna, Herman Geuvers
A Real Semantic Web for Mathematics Deserves a Real Semantics. SemWiki (2008)
S. Barry Cooper, Herman Geuvers, Anand Pillay, Jouko A. Väänänen
Preface. Ann. Pure Appl. Log. 156 (1) (2008)
Bas Spitters, Herman Geuvers, Milad Niqui, Freek Wiedijk
Preface to the special issue: Constructive analysis, types and exact real numbers. Math. Struct. Comput. Sci. 17 (1) (2007)
Herman Geuvers, Iris Loeb
Natural deduction via graphs: formal definition and computation rules. Math. Struct. Comput. Sci. 17 (3) (2007)
Herman Geuvers, Milad Niqui, Bas Spitters, Freek Wiedijk
Constructive analysis, types and exact real numbers. Math. Struct. Comput. Sci. 17 (1) (2007)
Herman Geuvers, Iris Loeb
From Deduction Graphs to Proof Nets: Boxes and Sharing in the Graphical Presentation of Deductions. MFCS (2006)
Herman Geuvers
(In)consistency of Extensions of Higher Order Logic and Type Theory. TYPES (2006)
Andrea Asperti, Herman Geuvers, Iris Loeb, Lionel Elie Mamane, Claudio Sacerdoti Coen
An Interactive Algebra Course with Formalised Proofs and Definitions. MKM (2005)
Luís Cruz-Filipe, Herman Geuvers, Freek Wiedijk
C-CoRN, the Constructive Coq Repository at Nijmegen. MKM (2004)
Herman Geuvers, Rob Nederpelt
Rewriting for Fitch Style Natural Deductions. RTA (2004)
Gueorgui I. Jojgov, Herman Geuvers
A Calculus of Tactics and Its Operational Semantics. Electron. Notes Theor. Comput. Sci. 93 (2004)
Herman Geuvers, Fairouz Kamareddine
Preface. Electron. Notes Theor. Comput. Sci. 85 (7) (2003)
Herman Geuvers, Randy Pollack, Freek Wiedijk, Jan Zwanenburg
A Constructive Algebraic Hierarchy in Coq. J. Symb. Comput. 34 (4) (2002)
Martijn Oostdijk, Herman Geuvers
Proof by computation in the Coq system. Theor. Comput. Sci. 272 (1-2) (2002)
Herman Geuvers, Gueorgui I. Jojgov
Open Proofs and Open Terms: A Basis for Interactive Logic. CSL (2002)
Herman Geuvers
Induction Is Not Derivable in Second Order Dependent Type Theory. TLCA (2001)
Herman Geuvers, Freek Wiedijk, Jan Zwanenburg
A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals. TYPES (2000)
Herman Geuvers, Milad Niqui
Constructive Reals in Coq: Axioms and Categoricity. TYPES (2000)
Herman Geuvers, Freek Wiedijk, Jan Zwanenburg
Equational Reasoning via Partial Reflection. TPHOLs (2000)
Herman Geuvers, Erik Poll, Jan Zwanenburg
Safe Proof Checking in Type Theory with Y. CSL (1999)
Herman Geuvers, Erik Barendsen
Some logical and syntactical observations concerning the first-order dependent type system lambda-P. Math. Struct. Comput. Sci. 9 (4) (1999)
Roel Bloo, Herman Geuvers
Explicit Substitution On the Edge of Strong Normalization. Theor. Comput. Sci. 211 (1-2) (1999)
Franco Barbanera, Maribel Fernández, Herman Geuvers
Modularity of Strong Normalization in the Algebraic-lambda-Cube. J. Funct. Program. 7 (6) (1997)
Herman Geuvers
Extending Models of Second Order Predicate Logic to Models of Second Dependent Type Theory. CSL (1996)
Gilles Barthe, Herman Geuvers
Modular Properties of Algebraic Type Systems. HOA (1995)
Gilles Barthe, Herman Geuvers
Congruence Types. CSL (1995)
Milena Stefanova, Herman Geuvers
A Simple Model Construction for the Calculus of Constructions. TYPES (1995)
Franco Barbanera, Maribel Fernández, Herman Geuvers
Modularity of Strong Normalization and Confluence in the algebraic-lambda-Cube LICS (1994)
Herman Geuvers, Benjamin Werner
On the Church-Rosser Property for Expressive Type Systems and its Consequences for their Metatheoretic Study LICS (1994)
Herman Geuvers
A short and flexible proof of Strong Normalization for the Calculus of Constructions. TYPES (1994)
Herman Geuvers
Conservativity between Logics and Typed lambda Calculi. TYPES (1993)
Herman Geuvers
The Church-Rosser Property for beta-eta-reduction in Typed lambda-Calculi LICS (1992)
Herman Geuvers, Mark-Jan Nederhof
Modular Proof of Strong Normalization for the Calculus of Constructions. J. Funct. Program. 1 (2) (1991)