Herman Geuvers

Herman Geuvers, Robbert Krebbers, James McKinna: The λμ^T-calculus. Ann. Pure Appl. Logic 164(6): 676-701 (2013)

Carst Tankink, Herman Geuvers, James McKinna: Narrating Formal Proof (Work in Progress). Electr. Notes Theor. Comput. Sci. 285: 71-83 (2012)

Herman Geuvers, Ugo de'Liguoro (Eds.): Proceedings Fourth Workshop on Classical Logic and Computation. EPTCS 97, 2012

Herman Geuvers, Robbert Krebbers, James McKinna: The lambda-mu-T-calculus. CoRR abs/1204.0347 (2012)

Jörg Endrullis, Herman Geuvers, Jakob Grue Simonsen, Hans Zantema: Levels of undecidability in rewriting. Inf. Comput. 209(2): 227-245 (2011)

Herman Geuvers, Robbert Krebbers: The correctness of Newman's typability algorithm and some of its extensions. Theor. Comput. Sci. 412(28): 3242-3261 (2011)

Daniel Kühlwein, Josef Urban, Evgeni Tsivtsivadze, Herman Geuvers, Tom Heskes: Multi-output Ranking for Automated Reasoning. KDIR 2011: 42-51

Daniel Kühlwein, Josef Urban, Evgeni Tsivtsivadze, Herman Geuvers, Tom Heskes: Learning2Reason. Calculemus/MKM 2011: 298-300

Evgeni Tsivtsivadze, Josef Urban, Herman Geuvers, Tom Heskes: Semantic Graph Kernels for Automated Reasoning. SDM 2011: 795-803

Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, Freek Wiedijk (Eds.): 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

Herman Geuvers, Gopalan Nadathur (Eds.): Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice. EPTCS 71, 2011

Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk: Proviola: A Tool for Proof Re-animation. AISC/MKM/Calculemus 2010: 440-454

Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers: A Wiki for Mizar: Motivation, Considerations, and Initial Prototype. AISC/MKM/Calculemus 2010: 455-469

Herman Geuvers, Adam Koprowski, Dan Synek, Eelis van der Weegen: Automated Machine-Checked Hybrid System Safety Proofs. ITP 2010: 259-274

Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk: Pure Type Systems without Explicit Contexts. LFMTP 2010: 53-67

Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk: Proviola: A Tool for Proof Re-animation. CoRR abs/1005.2672 (2010)

Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers: A Wiki for Mizar: Motivation, Considerations, and Initial Prototype. CoRR abs/1005.4552 (2010)

Andrea Asperti, Herman Geuvers, Raja Natarajan: Social processes, program verification and all that. Mathematical Structures in Computer Science 19(5): 877-896 (2009)

Jörg Endrullis, Herman Geuvers, Hans Zantema: Degrees of Undecidability in Term Rewriting. CSL 2009: 255-270

Lionel Elie Mamane, Herman Geuvers, James McKinna: A Logically Saturated Extension of lambdaµµ. Calculemus/MKM 2009: 405-421

Jörg Endrullis, Herman Geuvers, Hans Zantema: Degrees of Undecidability in Rewriting. CoRR abs/0902.4723 (2009)

S. Barry Cooper, Herman Geuvers, Anand Pillay, Jouko A. Väänänen: Preface. Ann. Pure Appl. Logic 156(1): 1-2 (2008)

Herman Geuvers, Freek Wiedijk: A Logical Framework with Explicit Conversions. Electr. Notes Theor. Comput. Sci. 199: 33-47 (2008)

Herman Geuvers, Iris Loeb: Deduction Graphs with Universal Quantification. Electr. Notes Theor. Comput. Sci. 203(1): 93-108 (2008)

Herman Geuvers: Introduction to Type Theory. LerNet ALFA Summer School 2008: 1-56

Cezary Kaliszyk, Pierre Corbineau, Freek Wiedijk, James McKinna, Herman Geuvers: A Real Semantic Web for Mathematics Deserves a Real Semantics. SemWiki 2008

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)

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)

Herman Geuvers, Iris Loeb: Natural deduction via graphs: formal definition and computation rules. Mathematical Structures in Computer Science 17(3): 485-526 (2007)

Herman Geuvers, Iris Loeb: From Deduction Graphs to Proof Nets: Boxes and Sharing in the Graphical Presentation of Deductions. MFCS 2006: 39-57

Herman Geuvers: (In)consistency of Extensions of Higher Order Logic and Type Theory. TYPES 2006: 140-159

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

Gueorgui I. Jojgov, Herman Geuvers: A Calculus of Tactics and Its Operational Semantics. Electr. Notes Theor. Comput. Sci. 93: 118-137 (2004)

Luís Cruz-Filipe, Herman Geuvers, Freek Wiedijk: C-CoRN, the Constructive Coq Repository at Nijmegen. MKM 2004: 88-103

Herman Geuvers, Rob Nederpelt: Rewriting for Fitch Style Natural Deductions. RTA 2004: 134-154

Herman Geuvers, Fairouz Kamareddine: Preface. Electr. Notes Theor. Comput. Sci. 85(7): 146-147 (2003)

Herman Geuvers, Freek Wiedijk (Eds.): 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

Herman Geuvers, Randy Pollack, Freek Wiedijk, Jan Zwanenburg: A Constructive Algebraic Hierarchy in Coq. J. Symb. Comput. 34(4): 271-286 (2002)

Martijn Oostdijk, Herman Geuvers: Proof by computation in the Coq system. Theor. Comput. Sci. 272(1-2): 293-314 (2002)

Herman Geuvers, Gueorgui I. Jojgov: Open Proofs and Open Terms: A Basis for Interactive Logic. CSL 2002: 537-552

Henk Barendregt, Herman Geuvers: Proof-Assistants Using Dependent Type Systems. Handbook of Automated Reasoning 2001: 1149-1238

Herman Geuvers: Induction Is Not Derivable in Second Order Dependent Type Theory. TLCA 2001: 166-181

Herman Geuvers, Freek Wiedijk, Jan Zwanenburg: Equational Reasoning via Partial Reflection. TPHOLs 2000: 162-178

Herman Geuvers, Milad Niqui: Constructive Reals in Coq: Axioms and Categoricity. TYPES 2000: 79-95

Herman Geuvers, Freek Wiedijk, Jan Zwanenburg: A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals. TYPES 2000: 96-111

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)

Roel Bloo, Herman Geuvers: Explicit Substitution On the Edge of Strong Normalization. Theor. Comput. Sci. 211(1-2): 375-395 (1999)

Herman Geuvers, Erik Poll, Jan Zwanenburg: Safe Proof Checking in Type Theory with Y. CSL 1999: 439-452

Franco Barbanera, Maribel Fernández, Herman Geuvers: Modularity of Strong Normalization in the Algebraic-lambda-Cube. J. Funct. Program. 7(6): 613-660 (1997)

Herman Geuvers: Extending Models of Second Order Predicate Logic to Models of Second Dependent Type Theory. CSL 1996: 167-181

Gilles Barthe, Herman Geuvers: Congruence Types. CSL 1995: 36-51

Gilles Barthe, Herman Geuvers: Modular Properties of Algebraic Type Systems. HOA 1995: 37-56

Milena Stefanova, Herman Geuvers: A Simple Model Construction for the Calculus of Constructions. TYPES 1995: 249-264

Herman Geuvers, Benjamin Werner: On the Church-Rosser Property for Expressive Type Systems and its Consequences for their Metatheoretic Study. LICS 1994: 320-329

Franco Barbanera, Maribel Fernández, Herman Geuvers: Modularity of Strong Normalization and Confluence in the algebraic-lambda-Cube. LICS 1994: 406-415

Herman Geuvers: A short and flexible proof of Strong Normalization for the Calculus of Constructions. TYPES 1994: 14-38

Herman Geuvers: Conservativity between Logics and Typed lambda Calculi. TYPES 1993: 79-107

Herman Geuvers: The Church-Rosser Property for beta-eta-reduction in Typed lambda-Calculi. LICS 1992: 453-460

Herman Geuvers, Mark-Jan Nederhof: Modular Proof of Strong Normalization for the Calculus of Constructions. J. Funct. Program. 1(2): 155-189 (1991)