Herman Geuvers

According to our database, Herman Geuvers authored at least 81 papers between 1991 and 2025.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of three.

2025

Initial Algebras of Domains via Quotient Inductive-Inductive Types.

Simcha van Collem, Niels van der Weide, Herman Geuvers

CoRR, September, 2025

Master Thesis Impredicative Encodings of Inductive and Coinductive Types.

Steven Bronsveld, Herman Geuvers, Niels van der Weide

CoRR, May, 2025

Impredicative Encodings of Inductive and Coinductive Types.

Steven Bronsveld, Herman Geuvers, Niels van der Weide

Proceedings of the 10th International Conference on Formal Structures for Computation and Deduction, 2025

2024

Hashing Modulo Context-Sensitive 𝛼-Equivalence.

Lasse Blaauwbroek, Miroslav Olsák, Herman Geuvers

Proc. ACM Program. Lang., 2024

2022

Characteristics of de Bruijn's early proof checker Automath.

Herman Geuvers, Rob Nederpelt

Fundam. Informaticae, 2022

Directed branching bisimulation via apartness and positive logic.

Herman Geuvers, Anton Golov

CoRR, 2022

Classical Natural Deduction from Truth Tables.

Herman Geuvers, Tonny Hurkens

Proceedings of the 28th International Conference on Types for Proofs and Programs, 2022

Diaframe: automated verification of fine-grained concurrent programs in Iris.

Ike Mulder, Robbert Krebbers, Herman Geuvers

Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

Apartness and Distinguishing Formulas in Hennessy-Milner Logic.

Herman Geuvers

Proceedings of the A Journey from Process Algebra via Timed Automata to Model Learning, 2022

2021

Relating Apartness and Bisimulation.

Herman Geuvers, Bart Jacobs

Log. Methods Comput. Sci., 2021

2020

The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq.

Lasse Blaauwbroek, Josef Urban, Herman Geuvers

CoRR, 2020

The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq.

Lasse Blaauwbroek, Josef Urban, Herman Geuvers

Proceedings of the Intelligent Computer Mathematics - 13th International Conference, 2020

Tactic Learning and Proving for the Coq Proof Assistant.

Lasse Blaauwbroek, Josef Urban, Herman Geuvers

Proceedings of the LPAR 2020: 23rd International Conference on Logic for Programming, 2020

2019

Strong Normalization for Truth Table Natural Deduction.

Herman Geuvers, Iris van der Giessen, Tonny Hurkens

Fundam. Informaticae, 2019

The Construction of Set-Truncated Higher Inductive Types.

Niels van der Weide, Herman Geuvers

Proceedings of the Thirty-Fifth Conference on the Mathematical Foundations of Programming Semantics, 2019

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

2018

Finite sets in homotopy type theory.

Dan Frumin, Herman Geuvers, Léon Gondelman, Niels van der Weide

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2017

Higher Inductive Types in Programming.

Henning Basold, Herman Geuvers, Niels van der Weide

J. Univers. Comput. Sci., 2017

Proof Terms for Generalized Natural Deduction.

Herman Geuvers, Tonny Hurkens

Proceedings of the 23rd International Conference on Types for Proofs and Programs, 2017

A Formalisation of Consistent Consequence for Boolean Equation Systems.

Myrthe van Delft, Herman Geuvers, Tim A. C. Willemse

Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

Deriving Natural Deduction Rules from Truth Tables.

Herman Geuvers, Tonny Hurkens

Proceedings of the Logic and Its Applications - 7th Indian Conference, 2017

2016

Type Theory based on Dependent Inductive and Coinductive Types.

Henning Basold, Herman Geuvers

Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

2014

A type system for Continuation Calculus.

Herman Geuvers, Wouter Geraedts, Bram Geron, Judith van Stegeren

Proceedings of the Proceedings Fifth International Workshop on Classical Logic and Computation, 2014

Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description.

Cezary Kaliszyk, Josef Urban, Jirí Vyskocil, Herman Geuvers

Proceedings of the Intelligent Computer Mathematics - International Conference, 2014

2013

Continuation calculus.

Bram Geron, Herman Geuvers

Proceedings of the Proceedings First Workshop on Control Operators and their Semantics, 2013

The <i>λ</i><i>μ</i>^<i>T</i>-calculus.

Herman Geuvers, Robbert Krebbers, James McKinna

Ann. Pure Appl. Log., 2013

Formal Mathematics on Display: A Wiki for Flyspeck.

Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers

Proceedings of the Intelligent Computer Mathematics, 2013

Explicit convertibility proofs in pure type systems.

Floris van Doorn, Herman Geuvers, Freek Wiedijk

Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, 2013

Communicating Formal Proofs: The Case of Flyspeck.

Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012

The lambda-mu-T-calculus

Herman Geuvers, Robbert Krebbers, James McKinna

CoRR, 2012

2011

The correctness of Newman's typability algorithm and some of its extensions.

Herman Geuvers, Robbert Krebbers

Theor. Comput. Sci., 2011

Levels of undecidability in rewriting.

Jörg Endrullis, Herman Geuvers, Jakob Grue Simonsen, Hans Zantema

Inf. Comput., 2011

Semantic Graph Kernels for Automated Reasoning.

Evgeni Tsivtsivadze, Josef Urban, Herman Geuvers, Tom Heskes

Proceedings of the Eleventh SIAM International Conference on Data Mining, 2011

Learning2Reason.

Daniel Kühlwein, Josef Urban, Evgeni Tsivtsivadze, Herman Geuvers, Tom Heskes

Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

Multi-output Ranking for Automated Reasoning.

Daniel Kühlwein, Josef Urban, Evgeni Tsivtsivadze, Herman Geuvers, Tom Heskes

Proceedings of the KDIR 2011, 2011

2010

Narrating Formal Proof (Work in Progress).

Carst Tankink, Herman Geuvers, James McKinna

Proceedings of the 9th International Workshop On User Interfaces for Theorem Provers, 2010

Pure Type Systems without Explicit Contexts

Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk

Proceedings of the Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, 2010

Automated Machine-Checked Hybrid System Safety Proofs.

Herman Geuvers, Adam Koprowski, Dan Synek, Eelis van der Weegen

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

A Wiki for Mizar: Motivation, Considerations, and Initial Prototype.

Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers

Proceedings of the Intelligent Computer Mathematics, 10th International Conference, 2010

Proviola: A Tool for Proof Re-animation.

Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk

Proceedings of the Intelligent Computer Mathematics, 10th International Conference, 2010

2009

Social processes, program verification and all that.

Andrea Asperti, Herman Geuvers, Raja Natarajan

Math. Struct. Comput. Sci., 2009

Degrees of Undecidability in Rewriting

Jörg Endrullis, Herman Geuvers, Hans Zantema

CoRR, 2009

A Logically Saturated Extension of lambdaµµ.

Lionel Elie Mamane, Herman Geuvers, James McKinna

Proceedings of the Intelligent Computer Mathematics, 2009

Degrees of Undecidability in Term Rewriting.

Jörg Endrullis, Herman Geuvers, Hans Zantema

Proceedings of the Computer Science Logic, 23rd international Workshop, 2009

2008

Preface.

S. Barry Cooper, Herman Geuvers, Anand Pillay, Jouko A. Väänänen

Ann. Pure Appl. Log., 2008

A Real Semantic Web for Mathematics Deserves a Real Semantics.

Cezary Kaliszyk, Pierre Corbineau, Freek Wiedijk, James McKinna, Herman Geuvers

Proceedings of the 3rd Semantic Wiki Workshop (SemWiki 2008) at the 5th European Semantic Web Conference (ESWC 2008), 2008

Introduction to Type Theory.

Herman Geuvers

Proceedings of the Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24, 2008

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

Constructive analysis, types and exact real numbers.

Herman Geuvers, Milad Niqui, Bas Spitters, Freek Wiedijk

Math. Struct. Comput. Sci., 2007

Natural deduction via graphs: formal definition and computation rules.

Herman Geuvers, Iris Loeb

Math. Struct. Comput. Sci., 2007

Deduction Graphs with Universal Quantification.

Herman Geuvers, Iris Loeb

Proceedings of the Fourth International Workshop on Computing with Terms and Graphs, 2007

2006

(In)consistency of Extensions of Higher Order Logic and Type Theory.

Herman Geuvers

Proceedings of the Types for Proofs and Programs, International Workshop, 2006

From Deduction Graphs to Proof Nets: Boxes and Sharing in the Graphical Presentation of Deductions.

Herman Geuvers, Iris Loeb

Proceedings of the Mathematical Foundations of Computer Science 2006, 2006

2005

An Interactive Algebra Course with Formalised Proofs and Definitions.

Andrea Asperti, Herman Geuvers, Iris Loeb, Lionel Elie Mamane, Claudio Sacerdoti Coen

Proceedings of the Mathematical Knowledge Management, 4th International Conference, 2005

2004

A Logical Framework with Explicit Conversions.

Herman Geuvers, Freek Wiedijk

Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages, 2004

Rewriting for Fitch Style Natural Deductions.

Herman Geuvers, Rob Nederpelt

Proceedings of the Rewriting Techniques and Applications, 15th International Conference, 2004

C-CoRN, the Constructive Coq Repository at Nijmegen.

Luís Cruz-Filipe, Herman Geuvers, Freek Wiedijk

Proceedings of the Mathematical Knowledge Management, Third International Conference, 2004

2003

A Calculus of Tactics and Its Operational Semantics.

Gueorgui I. Jojgov, Herman Geuvers

Proceedings of the Mathematical Knowledge Management Symposium, 2003

Preface.

Herman Geuvers, Fairouz Kamareddine

Proceedings of the Mathematics, 2003

2002

Proof by computation in the Coq system.

Martijn Oostdijk, Herman Geuvers

Theor. Comput. Sci., 2002

A Constructive Algebraic Hierarchy in Coq.

Herman Geuvers, Randy Pollack, Freek Wiedijk, Jan Zwanenburg

J. Symb. Comput., 2002

Open Proofs and Open Terms: A Basis for Interactive Logic.

Herman Geuvers, Gueorgui I. Jojgov

Proceedings of the Computer Science Logic, 16th International Workshop, 2002

2001

Induction Is Not Derivable in Second Order Dependent Type Theory.

Herman Geuvers

Proceedings of the Typed Lambda Calculi and Applications, 5th International Conference, 2001

Proof-Assistants Using Dependent Type Systems.

Henk Barendregt, Herman Geuvers

Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

2000

A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals.

Herman Geuvers, Freek Wiedijk, Jan Zwanenburg

Proceedings of the Types for Proofs and Programs, International Workshop, 2000

Constructive Reals in Coq: Axioms and Categoricity.

Herman Geuvers, Milad Niqui

Proceedings of the Types for Proofs and Programs, International Workshop, 2000

Equational Reasoning via Partial Reflection.

Herman Geuvers, Freek Wiedijk, Jan Zwanenburg

Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000

1999

Explicit Substitution On the Edge of Strong Normalization.

Roel Bloo, Herman Geuvers

Theor. Comput. Sci., 1999

Some logical and syntactical observations concerning the first-order dependent type system lambda-P.

Herman Geuvers, Erik Barendsen

Math. Struct. Comput. Sci., 1999

Safe Proof Checking in Type Theory with Y.

Herman Geuvers, Erik Poll, Jan Zwanenburg

Proceedings of the Computer Science Logic, 13th International Workshop, 1999

1997

Modularity of Strong Normalization in the Algebraic-lambda-Cube.

Franco Barbanera, Maribel Fernández, Herman Geuvers

J. Funct. Program., 1997

1996

Extending Models of Second Order Predicate Logic to Models of Second Dependent Type Theory.

Herman Geuvers

Proceedings of the Computer Science Logic, 10th International Workshop, 1996

1995

A Simple Model Construction for the Calculus of Constructions.

Milena Stefanova, Herman Geuvers

Proceedings of the Types for Proofs and Programs, 1995

Modular Properties of Algebraic Type Systems.

Gilles Barthe, Herman Geuvers

Proceedings of the Higher-Order Algebra, 1995

Congruence Types.

Gilles Barthe, Herman Geuvers

Proceedings of the Computer Science Logic, 9th International Workshop, 1995

1994

A short and flexible proof of Strong Normalization for the Calculus of Constructions.

Herman Geuvers

Proceedings of the Types for Proofs and Programs, 1994

On the Church-Rosser Property for Expressive Type Systems and its Consequences for their Metatheoretic Study

Herman Geuvers, Benjamin Werner

Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), 1994

Modularity of Strong Normalization and Confluence in the algebraic-lambda-Cube

Franco Barbanera, Maribel Fernández, Herman Geuvers

Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), 1994

1993

Conservativity between Logics and Typed lambda Calculi.

Herman Geuvers

Proceedings of the Types for Proofs and Programs, 1993

1992

The Church-Rosser Property for beta-eta-reduction in Typed lambda-Calculi

Herman Geuvers

Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS '92), 1992

1991

Modular Proof of Strong Normalization for the Calculus of Constructions.

Herman Geuvers, Mark-Jan Nederhof

J. Funct. Program., 1991