Please note: This is a beta version of the new dblp website.
You can find the classic dblp view of this page here.
You can find the classic dblp view of this page here.
Herman Geuvers
2010 – today
- 2013
[j19]Herman Geuvers, Robbert Krebbers, James McKinna: The λμT-calculus. Ann. Pure Appl. Logic 164(6): 676-701 (2013)- [c33]Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers: Communicating Formal Proofs: The Case of Flyspeck. ITP 2013: 451-456
- [c32]Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers: Formal Mathematics on Display: A Wiki for Flyspeck. MKM/Calculemus/DML 2013: 152-167
- [i6]Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers: Formal Mathematics on Display: A Wiki for Flyspeck. CoRR abs/1305.5710 (2013)
- [i5]
- 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 (Eds.): Proceedings Fourth Workshop on Classical Logic and Computation. EPTCS 97, 2012
- [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 (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
- [e2]Herman Geuvers, Gopalan Nadathur (Eds.): Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice. EPTCS 71, 2011
- 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 (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
- 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
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-10-17 21:25 CEST by the dblp team