default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDHerman Geuvers
Person information
- affiliation: Eindhoven University of Technology, The Netherlands
- affiliation: Radboud University Nijmegen, The Netherlands
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
Journal Articles
- 2024
[j19]Lasse Blaauwbroek
, Miroslav Olsák, Herman Geuvers:
Hashing Modulo Context-Sensitive 𝛼-Equivalence. Proc. ACM Program. Lang. 8(PLDI): 2027-2050 (2024)- 2022
- [j18]Herman Geuvers, Rob Nederpelt:
Characteristics of de Bruijn's early proof checker Automath. Fundam. Informaticae 185(4): 313-336 (2022) - 2021
- [j17]Herman Geuvers, Bart Jacobs:
Relating Apartness and Bisimulation. Log. Methods Comput. Sci. 17(3) (2021) - 2019
- [j16]Herman Geuvers, Iris van der Giessen, Tonny Hurkens:
Strong Normalization for Truth Table Natural Deduction. Fundam. Informaticae 170(1-3): 139-176 (2019) - 2017
- [j15]Henning Basold, Herman Geuvers, Niels van der Weide:
Higher Inductive Types in Programming. J. Univers. Comput. Sci. 23(1): 63-88 (2017) - 2013
- [j14]Herman Geuvers, Robbert Krebbers, James McKinna:
The λμT-calculus. Ann. Pure Appl. Log. 164(6): 676-701 (2013) - 2011
- [j13]Jörg Endrullis, Herman Geuvers, Jakob Grue Simonsen, Hans Zantema:
Levels of undecidability in rewriting. Inf. Comput. 209(2): 227-245 (2011) - [j12]Herman Geuvers, Robbert Krebbers:
The correctness of Newman's typability algorithm and some of its extensions. Theor. Comput. Sci. 412(28): 3242-3261 (2011) - 2009
- [j11]Andrea Asperti, Herman Geuvers, Raja Natarajan:
Social processes, program verification and all that. Math. Struct. Comput. Sci. 19(5): 877-896 (2009) - 2008
- [j10]S. Barry Cooper, Herman Geuvers, Anand Pillay, Jouko A. Väänänen:
Preface. Ann. Pure Appl. Log. 156(1): 1-2 (2008) - 2007
- [j9]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): 1 (2007) - [j8]Herman Geuvers, Milad Niqui, Bas Spitters, Freek Wiedijk:
Constructive analysis, types and exact real numbers. Math. Struct. Comput. Sci. 17(1): 3-36 (2007) - [j7]Herman Geuvers, Iris Loeb:
Natural deduction via graphs: formal definition and computation rules. Math. Struct. Comput. Sci. 17(3): 485-526 (2007) - 2002
- [j6]Herman Geuvers, Randy Pollack, Freek Wiedijk, Jan Zwanenburg:
A Constructive Algebraic Hierarchy in Coq. J. Symb. Comput. 34(4): 271-286 (2002) - [j5]Martijn Oostdijk, Herman Geuvers:
Proof by computation in the Coq system. Theor. Comput. Sci. 272(1-2): 293-314 (2002) - 1999
- [j4]Herman Geuvers, Erik Barendsen:
Some logical and syntactical observations concerning the first-order dependent type system lambda-P. Math. Struct. Comput. Sci. 9(4): 335-359 (1999) - [j3]Roel Bloo, Herman Geuvers:
Explicit Substitution On the Edge of Strong Normalization. Theor. Comput. Sci. 211(1-2): 375-395 (1999) - 1997
- [j2]Franco Barbanera, Maribel Fernández, Herman Geuvers:
Modularity of Strong Normalization in the Algebraic-lambda-Cube. J. Funct. Program. 7(6): 613-660 (1997) - 1991
- [j1]Herman Geuvers, Mark-Jan Nederhof:
Modular Proof of Strong Normalization for the Calculus of Constructions. J. Funct. Program. 1(2): 155-189 (1991)
Conference and Workshop Papers
- 2022
- [c53]Herman Geuvers:
Apartness and Distinguishing Formulas in Hennessy-Milner Logic. A Journey from Process Algebra via Timed Automata to Model Learning 2022: 266-282 - [c52]Ike Mulder, Robbert Krebbers, Herman Geuvers:
Diaframe: automated verification of fine-grained concurrent programs in Iris. PLDI 2022: 809-824 - [c51]Herman Geuvers, Tonny Hurkens:
Classical Natural Deduction from Truth Tables. TYPES 2022: 2:1-2:27 - 2020
- [c50]Lasse Blaauwbroek, Josef Urban, Herman Geuvers:
Tactic Learning and Proving for the Coq Proof Assistant. LPAR 2020: 138-150 - [c49]Lasse Blaauwbroek, Josef Urban, Herman Geuvers:
The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq. CICM 2020: 271-277 - 2019
- [c48]Niels van der Weide, Herman Geuvers:
The Construction of Set-Truncated Higher Inductive Types. MFPS 2019: 261-280 - 2018
- [c47]Dan Frumin, Herman Geuvers, Léon Gondelman, Niels van der Weide:
Finite sets in homotopy type theory. CPP 2018: 201-214 - 2017
- [c46]Herman Geuvers, Tonny Hurkens:
Deriving Natural Deduction Rules from Truth Tables. ICLA 2017: 123-138 - [c45]Myrthe van Delft, Herman Geuvers, Tim A. C. Willemse:
A Formalisation of Consistent Consequence for Boolean Equation Systems. ITP 2017: 462-478 - [c44]Herman Geuvers, Tonny Hurkens:
Proof Terms for Generalized Natural Deduction. TYPES 2017: 3:1-3:39 - 2016
- [c43]Henning Basold, Herman Geuvers:
Type Theory based on Dependent Inductive and Coinductive Types. LICS 2016: 327-336 - 2014
- [c42]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil, Herman Geuvers:
Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description. CICM 2014: 435-439 - [c41]Herman Geuvers, Wouter Geraedts, Bram Geron, Judith van Stegeren:
A type system for Continuation Calculus. CL&C 2014: 1-17 - 2013
- [c40]Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers:
Communicating Formal Proofs: The Case of Flyspeck. ITP 2013: 451-456 - [c39]Floris van Doorn, Herman Geuvers, Freek Wiedijk:
Explicit convertibility proofs in pure type systems. LFMTP 2013: 25-36 - [c38]Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers:
Formal Mathematics on Display: A Wiki for Flyspeck. MKM/Calculemus/DML 2013: 152-167 - [c37]Bram Geron, Herman Geuvers:
Continuation calculus. COS 2013: 66-85 - 2011
- [c36]Daniel Kühlwein, Josef Urban, Evgeni Tsivtsivadze, Herman Geuvers, Tom Heskes:
Multi-output Ranking for Automated Reasoning. KDIR 2011: 42-51 - [c35]Daniel Kühlwein, Josef Urban, Evgeni Tsivtsivadze, Herman Geuvers, Tom Heskes:
Learning2Reason. Calculemus/MKM 2011: 298-300 - [c34]Evgeni Tsivtsivadze, Josef Urban, Herman Geuvers, Tom Heskes:
Semantic Graph Kernels for Automated Reasoning. SDM 2011: 795-803 - 2010
- [c33]Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk:
Proviola: A Tool for Proof Re-animation. AISC/MKM/Calculemus 2010: 440-454 - [c32]Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers:
A Wiki for Mizar: Motivation, Considerations, and Initial Prototype. AISC/MKM/Calculemus 2010: 455-469 - [c31]Herman Geuvers, Adam Koprowski, Dan Synek, Eelis van der Weegen:
Automated Machine-Checked Hybrid System Safety Proofs. ITP 2010: 259-274 - [c30]Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk:
Pure Type Systems without Explicit Contexts. LFMTP 2010: 53-67 - [c29]Carst Tankink, Herman Geuvers, James McKinna:
Narrating Formal Proof (Work in Progress). UITP 2010: 71-83 - 2009
- [c28]Jörg Endrullis, Herman Geuvers, Hans Zantema:
Degrees of Undecidability in Term Rewriting. CSL 2009: 255-270 - [c27]Lionel Elie Mamane, Herman Geuvers, James McKinna:
A Logically Saturated Extension of lambdaµµ. Calculemus/MKM 2009: 405-421 - 2008
- [c26]Herman Geuvers:
Introduction to Type Theory. LerNet ALFA Summer School 2008: 1-56 - [c25]Cezary Kaliszyk, Pierre Corbineau, Freek Wiedijk, James McKinna, Herman Geuvers:
A Real Semantic Web for Mathematics Deserves a Real Semantics. SemWiki 2008 - 2007
- [c24]Herman Geuvers, Iris Loeb:
Deduction Graphs with Universal Quantification. TERMGRAPH@ETAPS 2007: 93-108 - 2006
- [c23]Herman Geuvers, Iris Loeb:
From Deduction Graphs to Proof Nets: Boxes and Sharing in the Graphical Presentation of Deductions. MFCS 2006: 39-57 - [c22]Herman Geuvers:
(In)consistency of Extensions of Higher Order Logic and Type Theory. TYPES 2006: 140-159 - 2005
- [c21]Andrea Asperti, Herman Geuvers, Iris Loeb, Lionel Elie Mamane, Claudio Sacerdoti Coen:
An Interactive Algebra Course with Formalised Proofs and Definitions. MKM 2005: 315-329 - 2004
- [c20]Luís Cruz-Filipe, Herman Geuvers, Freek Wiedijk:
C-CoRN, the Constructive Coq Repository at Nijmegen. MKM 2004: 88-103 - [c19]Herman Geuvers, Rob Nederpelt:
Rewriting for Fitch Style Natural Deductions. RTA 2004: 134-154 - [c18]Herman Geuvers, Freek Wiedijk:
A Logical Framework with Explicit Conversions. LFM@IJCAR 2004: 33-47 - 2003
- [c17]Gueorgui I. Jojgov, Herman Geuvers:
A Calculus of Tactics and Its Operational Semantics. MKM Symposium 2003: 118-137 - [c16]Herman Geuvers, Fairouz Kamareddine:
Preface. Mathematics, Logic and Computation @ ICALP 2003: 146-147 - 2002
- [c15]Herman Geuvers, Gueorgui I. Jojgov:
Open Proofs and Open Terms: A Basis for Interactive Logic. CSL 2002: 537-552 - 2001
- [c14]Herman Geuvers:
Induction Is Not Derivable in Second Order Dependent Type Theory. TLCA 2001: 166-181 - 2000
- [c13]Herman Geuvers, Freek Wiedijk, Jan Zwanenburg:
Equational Reasoning via Partial Reflection. TPHOLs 2000: 162-178 - [c12]Herman Geuvers, Milad Niqui:
Constructive Reals in Coq: Axioms and Categoricity. TYPES 2000: 79-95 - [c11]Herman Geuvers, Freek Wiedijk, Jan Zwanenburg:
A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals. TYPES 2000: 96-111 - 1999
- [c10]Herman Geuvers, Erik Poll, Jan Zwanenburg:
Safe Proof Checking in Type Theory with Y. CSL 1999: 439-452 - 1996
- [c9]Herman Geuvers:
Extending Models of Second Order Predicate Logic to Models of Second Dependent Type Theory. CSL 1996: 167-181 - 1995
- [c8]Gilles Barthe, Herman Geuvers:
Congruence Types. CSL 1995: 36-51 - [c7]Gilles Barthe, Herman Geuvers:
Modular Properties of Algebraic Type Systems. HOA 1995: 37-56 - [c6]Milena Stefanova, Herman Geuvers:
A Simple Model Construction for the Calculus of Constructions. TYPES 1995: 249-264 - 1994
- [c5]Herman Geuvers, Benjamin Werner:
On the Church-Rosser Property for Expressive Type Systems and its Consequences for their Metatheoretic Study. LICS 1994: 320-329 - [c4]Franco Barbanera, Maribel Fernández, Herman Geuvers:
Modularity of Strong Normalization and Confluence in the algebraic-lambda-Cube. LICS 1994: 406-415 - [c3]Herman Geuvers:
A short and flexible proof of Strong Normalization for the Calculus of Constructions. TYPES 1994: 14-38 - 1993
- [c2]Herman Geuvers:
Conservativity between Logics and Typed lambda Calculi. TYPES 1993: 79-107 - 1992
- [c1]Herman Geuvers:
The Church-Rosser Property for beta-eta-reduction in Typed lambda-Calculi. LICS 1992: 453-460
Parts in Books or Collections
- 2001
- [p1]Henk Barendregt, Herman Geuvers:
Proof-Assistants Using Dependent Type Systems. Handbook of Automated Reasoning 2001: 1149-1238
Editorship
- 2019
- [e8]Herman Geuvers:
4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany. LIPIcs 131, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2019, ISBN 978-3-95977-107-8 [contents] - 2018
- [e7]Silvia Ghilezan, Herman Geuvers, Jelena Ivetic:
22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia. LIPIcs 97, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2018, ISBN 978-3-95977-065-1 [contents] - 2017
- [e6]Herman Geuvers, Matthew England, Osman Hasan, Florian Rabe, Olaf Teschke:
Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings. Lecture Notes in Computer Science 10383, Springer 2017, ISBN 978-3-319-62074-9 [contents] - 2012
- [e5]Herman Geuvers, Ugo de'Liguoro:
Proceedings Fourth Workshop on Classical Logic and Computation, CL&C 2012, Warwick, England, 8th July 2012. EPTCS 97, 2012 [contents] - 2011
- [e4]Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, Freek Wiedijk:
Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings. Lecture Notes in Computer Science 6898, Springer 2011, ISBN 978-3-642-22862-9 [contents] - [e3]Herman Geuvers, Gopalan Nadathur:
Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2011, Nijmegen, The Netherlands, August 26, 2011. EPTCS 71, 2011 [contents] - 2003
- [e2]Herman Geuvers, Fairouz Kamareddine:
Mathematics, Logic and Computation, Satellite Event of ICALP 2003, Eindhoven, The Netherlands, July 4-5, 2003. Electronic Notes in Theoretical Computer Science 85(7), Elsevier 2003 [contents] - [e1]Herman Geuvers, Freek Wiedijk:
Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers. Lecture Notes in Computer Science 2646, Springer 2003, ISBN 3-540-14031-X [contents]
Informal and Other Publications
- 2024
- [i14]Lasse Blaauwbroek, Miroslav Olsák, Herman Geuvers:
Hashing Modulo Context-Sensitive α-Equivalence. CoRR abs/2401.02948 (2024) - 2022
- [i13]Herman Geuvers, Rob Nederpelt:
Characteristics of de Bruijn's early proof checker Automath. CoRR abs/2203.01173 (2022) - [i12]Herman Geuvers, Anton Golov:
Directed branching bisimulation via apartness and positive logic. CoRR abs/2210.07380 (2022) - 2020
- [i11]Herman Geuvers, Bart Jacobs:
Relating Apartness and Bisimulation. CoRR abs/2002.02512 (2020) - [i10]Lasse Blaauwbroek, Josef Urban, Herman Geuvers:
Tactic Learning and Proving for the Coq Proof Assistant. CoRR abs/2003.09140 (2020) - [i9]Lasse Blaauwbroek, Josef Urban, Herman Geuvers:
The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq. CoRR abs/2008.00120 (2020) - 2019
- [i8]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 abs/1904.01009 (2019) - 2016
- [i7]Henning Basold, Herman Geuvers:
Type Theory based on Dependent Inductive and Coinductive Types. CoRR abs/1605.02206 (2016) - 2014
- [i6]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil, Herman Geuvers:
Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Description. CoRR abs/1405.3451 (2014) - 2013
- [i5]Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers:
Formal Mathematics on Display: A Wiki for Flyspeck. CoRR abs/1305.5710 (2013) - 2012
- [i4]Herman Geuvers, Robbert Krebbers, James McKinna:
The lambda-mu-T-calculus. CoRR abs/1204.0347 (2012) - 2010
- [i3]Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk:
Proviola: A Tool for Proof Re-animation. CoRR abs/1005.2672 (2010) - [i2]Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers:
A Wiki for Mizar: Motivation, Considerations, and Initial Prototype. CoRR abs/1005.4552 (2010) - 2009
- [i1]Jörg Endrullis, Herman Geuvers, Hans Zantema:
Degrees of Undecidability in Rewriting. CoRR abs/0902.4723 (2009)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-22 20:50 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
