Google
Google Scholar
MS Academic
CiteSeerX
CORE
Semantic ScholarHerman Geuvers
Person information
- affiliation: Eindhoven University of Technology, Netherlands
- affiliation: Radboud University Nijmegen, Netherlands
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
showing all ?? records
2010 – today
- 2018
[c41]Dan Frumin, Herman Geuvers, Léon Gondelman, Niels van der Weide:
Finite sets in homotopy type theory. CPP 2018: 201-214- 2017
- [j20]Henning Basold, Herman Geuvers, Niels van der Weide:
Higher Inductive Types in Programming. J. UCS 23(1): 63-88 (2017) - [c40]Herman Geuvers, Tonny Hurkens:
Deriving Natural Deduction Rules from Truth Tables. ICLA 2017: 123-138 - [c39]Myrthe van Delft, Herman Geuvers, Tim A. C. Willemse:
A Formalisation of Consistent Consequence for Boolean Equation Systems. ITP 2017: 462-478 - [e5]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] - 2016
- [c38]Henning Basold, Herman Geuvers:
Type Theory based on Dependent Inductive and Coinductive Types. LICS 2016: 327-336 - [i7]Henning Basold, Herman Geuvers:
Type Theory based on Dependent Inductive and Coinductive Types. CoRR abs/1605.02206 (2016) - 2014
- [c37]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil, Herman Geuvers:
Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description. CICM 2014: 435-439 - [c36]Herman Geuvers, Wouter Geraedts, Bram Geron, Judith van Stegeren:
A type system for Continuation Calculus. CL&C 2014: 1-17 - [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
- [j19]Herman Geuvers, Robbert Krebbers, James McKinna:
The λμT-calculus. Ann. Pure Appl. Logic 164(6): 676-701 (2013) - [c35]Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers:
Communicating Formal Proofs: The Case of Flyspeck. ITP 2013: 451-456 - [c34]Floris van Doorn, Herman Geuvers, Freek Wiedijk:
Explicit convertibility proofs in pure type systems. LFMTP 2013: 25-36 - [c33]Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers:
Formal Mathematics on Display: A Wiki for Flyspeck. MKM/Calculemus/DML 2013: 152-167 - [c32]
- [i5]Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers:
Formal Mathematics on Display: A Wiki for Flyspeck. CoRR abs/1305.5710 (2013) - 2012
- [j18]Carst Tankink, Herman Geuvers, James McKinna:
Narrating Formal Proof (Work in Progress). Electr. Notes Theor. Comput. Sci. 285: 71-83 (2012) - [e4]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] - [i4]Herman Geuvers, Robbert Krebbers, James McKinna:
The lambda-mu-T-calculus. CoRR abs/1204.0347 (2012) - 2011
- [j17]Jörg Endrullis, Herman Geuvers, Jakob Grue Simonsen, Hans Zantema:
Levels of undecidability in rewriting. Inf. Comput. 209(2): 227-245 (2011) - [j16]Herman Geuvers, Robbert Krebbers:
The correctness of Newman's typability algorithm and some of its extensions. Theor. Comput. Sci. 412(28): 3242-3261 (2011) - [c31]Daniel Kühlwein, Josef Urban, Evgeni Tsivtsivadze, Herman Geuvers, Tom Heskes:
Multi-output Ranking for Automated Reasoning. KDIR 2011: 42-51 - [c30]Daniel Kühlwein, Josef Urban, Evgeni Tsivtsivadze, Herman Geuvers, Tom Heskes:
Learning2Reason. Calculemus/MKM 2011: 298-300 - [c29]Evgeni Tsivtsivadze, Josef Urban, Herman Geuvers, Tom Heskes:
Semantic Graph Kernels for Automated Reasoning. SDM 2011: 795-803 - [e3]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] - [e2]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] - 2010
- [c28]Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk:
Proviola: A Tool for Proof Re-animation. AISC/MKM/Calculemus 2010: 440-454 - [c27]Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers:
A Wiki for Mizar: Motivation, Considerations, and Initial Prototype. AISC/MKM/Calculemus 2010: 455-469 - [c26]Herman Geuvers, Adam Koprowski, Dan Synek, Eelis van der Weegen:
Automated Machine-Checked Hybrid System Safety Proofs. ITP 2010: 259-274 - [c25]Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk:
Pure Type Systems without Explicit Contexts. LFMTP 2010: 53-67 - [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)
2000 – 2009
- 2009
- [j15]Andrea Asperti, Herman Geuvers, Raja Natarajan:
Social processes, program verification and all that. Mathematical Structures in Computer Science 19(5): 877-896 (2009) - [c24]Jörg Endrullis, Herman Geuvers, Hans Zantema:
Degrees of Undecidability in Term Rewriting. CSL 2009: 255-270 - [c23]Lionel Elie Mamane, Herman Geuvers, James McKinna:
A Logically Saturated Extension of lambdaµµ. Calculemus/MKM 2009: 405-421 - [i1]Jörg Endrullis, Herman Geuvers, Hans Zantema:
Degrees of Undecidability in Rewriting. CoRR abs/0902.4723 (2009) - 2008
- [j14]S. Barry Cooper, Herman Geuvers, Anand Pillay, Jouko A. Väänänen:
Preface. Ann. Pure Appl. Logic 156(1): 1-2 (2008) - [j13]Herman Geuvers, Freek Wiedijk:
A Logical Framework with Explicit Conversions. Electr. Notes Theor. Comput. Sci. 199: 33-47 (2008) - [j12]Herman Geuvers, Iris Loeb:
Deduction Graphs with Universal Quantification. Electr. Notes Theor. Comput. Sci. 203(1): 93-108 (2008) - [c22]
- [c21]Cezary Kaliszyk, Pierre Corbineau, Freek Wiedijk, James McKinna, Herman Geuvers:
A Real Semantic Web for Mathematics Deserves a Real Semantics. SemWiki 2008 - 2007
- [j11]Bas Spitters, Herman Geuvers, Milad Niqui, Freek Wiedijk:
Preface to the special issue: Constructive analysis, types and exact real numbers. Mathematical Structures in Computer Science 17(1): 1 (2007) - [j10]Herman Geuvers, Milad Niqui, Bas Spitters, Freek Wiedijk:
Constructive analysis, types and exact real numbers. Mathematical Structures in Computer Science 17(1): 3-36 (2007) - [j9]Herman Geuvers, Iris Loeb:
Natural deduction via graphs: formal definition and computation rules. Mathematical Structures in Computer Science 17(3): 485-526 (2007) - 2006
- [c20]
- [c19]Herman Geuvers:
(In)consistency of Extensions of Higher Order Logic and Type Theory. TYPES 2006: 140-159 - 2005
- [c18]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
- [j8]Gueorgui I. Jojgov, Herman Geuvers:
A Calculus of Tactics and Its Operational Semantics. Electr. Notes Theor. Comput. Sci. 93: 118-137 (2004) - [c17]Luís Cruz-Filipe, Herman Geuvers, Freek Wiedijk:
C-CoRN, the Constructive Coq Repository at Nijmegen. MKM 2004: 88-103 - [c16]
- 2003
- [j7]Herman Geuvers, Fairouz Kamareddine:
Preface. Electr. Notes Theor. Comput. Sci. 85(7): 146-147 (2003) - [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] - 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) - [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 - [p1]Henk Barendregt, Herman Geuvers:
Proof-Assistants Using Dependent Type Systems. Handbook of Automated Reasoning 2001: 1149-1238 - 2000
- [c13]Herman Geuvers, Freek Wiedijk, Jan Zwanenburg:
Equational Reasoning via Partial Reflection. TPHOLs 2000: 162-178 - [c12]
- [c11]Herman Geuvers, Freek Wiedijk, Jan Zwanenburg:
A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals. TYPES 2000: 96-111
1990 – 1999
- 1999
- [j4]Herman Geuvers, Erik Barendsen:
Some logical and syntactical observations concerning the first-order dependent type system lambda-P. Mathematical Structures in Computer Science 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) - [c10]Herman Geuvers, Erik Poll, Jan Zwanenburg:
Safe Proof Checking in Type Theory with Y. CSL 1999: 439-452 - 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) - 1996
- [c9]Herman Geuvers:
Extending Models of Second Order Predicate Logic to Models of Second Dependent Type Theory. CSL 1996: 167-181 - 1995
- [c8]
- [c7]
- [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]
- 1992
- [c1]Herman Geuvers:
The Church-Rosser Property for beta-eta-reduction in Typed lambda-Calculi. LICS 1992: 453-460 - 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)
Coauthor Index
maintained by 
at 
at 
data released under the ODC-BY 1.0 license; see also our legal information page
last updated on 2017-12-31 19:55 CET by the dblp team