 | 2009 |
|---|
| 41 |       | Jörg Endrullis,
Herman Geuvers,
Hans Zantema:
Degrees of Undecidability in Term Rewriting.
CSL 2009: 255-270 |
| 40 | | Lionel Elie Mamane,
Herman Geuvers,
James McKinna:
A Logically Saturated Extension of .
Calculemus/MKM 2009: 405-421 |
| 39 | | Jörg Endrullis,
Herman Geuvers,
Hans Zantema:
Degrees of Undecidability in Rewriting
CoRR abs/0902.4723: (2009) |
| 2008 |
|---|
| 38 | | Herman Geuvers:
Introduction to Type Theory.
LerNet ALFA Summer School 2008: 1-56 |
| 37 | | Cezary Kaliszyk,
Pierre Corbineau,
Freek Wiedijk,
James McKinna,
Herman Geuvers:
A Real Semantic Web for Mathematics Deserves a Real Semantics.
SemWiki 2008 |
| 36 | | S. Barry Cooper,
Herman Geuvers,
Anand Pillay,
Jouko A. Väänänen:
Preface.
Ann. Pure Appl. Logic 156(1): 1-2 (2008) |
| 35 | | Herman Geuvers,
Freek Wiedijk:
A Logical Framework with Explicit Conversions.
Electr. Notes Theor. Comput. Sci. 199: 33-47 (2008) |
| 34 | | Herman Geuvers,
Iris Loeb:
Deduction Graphs with Universal Quantification.
Electr. Notes Theor. Comput. Sci. 203(1): 93-108 (2008) |
| 2007 |
|---|
| 33 | | 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) |
| 32 | | 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) |
| 31 | | Herman Geuvers,
Iris Loeb:
Natural deduction via graphs: formal definition and computation rules.
Mathematical Structures in Computer Science 17(3): 485-526 (2007) |
| 2006 |
|---|
| 30 | | Herman Geuvers,
Iris Loeb:
From Deduction Graphs to Proof Nets: Boxes and Sharing in the Graphical Presentation of Deductions.
MFCS 2006: 39-57 |
| 29 | | Herman Geuvers:
(In)consistency of Extensions of Higher Order Logic and Type Theory.
TYPES 2006: 140-159 |
| 2005 |
|---|
| 28 | | 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 |
|---|
| 27 | | Luís Cruz-Filipe,
Herman Geuvers,
Freek Wiedijk:
C-CoRN, the Constructive Coq Repository at Nijmegen.
MKM 2004: 88-103 |
| 26 | | Herman Geuvers,
Rob Nederpelt:
Rewriting for Fitch Style Natural Deductions.
RTA 2004: 134-154 |
| 25 | | Gueorgui I. Jojgov,
Herman Geuvers:
A Calculus of Tactics and Its Operational Semantics.
Electr. Notes Theor. Comput. Sci. 93: 118-137 (2004) |
| 2003 |
|---|
| 24 |  | 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
Springer 2003 |
| 23 | | Herman Geuvers,
Fairouz Kamareddine:
Preface.
Electr. Notes Theor. Comput. Sci. 85(7): (2003) |
| 2002 |
|---|
| 22 | | Herman Geuvers,
Gueorgui I. Jojgov:
Open Proofs and Open Terms: A Basis for Interactive Logic.
CSL 2002: 537-552 |
| 21 | | Herman Geuvers,
Randy Pollack,
Freek Wiedijk,
Jan Zwanenburg:
A Constructive Algebraic Hierarchy in Coq.
J. Symb. Comput. 34(4): 271-286 (2002) |
| 20 | | Martijn Oostdijk,
Herman Geuvers:
Proof by computation in the Coq system.
Theor. Comput. Sci. 272(1-2): 293-314 (2002) |
| 2001 |
|---|
| 19 | | Herman Geuvers:
Induction Is Not Derivable in Second Order Dependent Type Theory.
TLCA 2001: 166-181 |
| 18 | | Henk Barendregt,
Herman Geuvers:
Proof-Assistants Using Dependent Type Systems.
Handbook of Automated Reasoning 2001: 1149-1238 |
| 2000 |
|---|
| 17 | | Herman Geuvers,
Freek Wiedijk,
Jan Zwanenburg:
Equational Reasoning via Partial Reflection.
TPHOLs 2000: 162-178 |
| 16 | | Herman Geuvers,
Milad Niqui:
Constructive Reals in Coq: Axioms and Categoricity.
TYPES 2000: 79-95 |
| 15 | | Herman Geuvers,
Freek Wiedijk,
Jan Zwanenburg:
A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals.
TYPES 2000: 96-111 |
| 1999 |
|---|
| 14 | | Herman Geuvers,
Erik Poll,
Jan Zwanenburg:
Safe Proof Checking in Type Theory with Y.
CSL 1999: 439-452 |
| 13 | | 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) |
| 12 | | Roel Bloo,
Herman Geuvers:
Explicit Substitution On the Edge of Strong Normalization.
Theor. Comput. Sci. 211(1-2): 375-395 (1999) |
| 1997 |
|---|
| 11 | | 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 |
|---|
| 10 | | Herman Geuvers:
Extending Models of Second Order Predicate Logic to Models of Second Dependent Type Theory.
CSL 1996: 167-181 |
| 1995 |
|---|
| 9 | | Gilles Barthe,
Herman Geuvers:
Congruence Types.
CSL 1995: 36-51 |
| 8 | | Gilles Barthe,
Herman Geuvers:
Modular Properties of Algebraic Type Systems.
HOA 1995: 37-56 |
| 7 | | Milena Stefanova,
Herman Geuvers:
A Simple Model Construction for the Calculus of Constructions.
TYPES 1995: 249-264 |
| 1994 |
|---|
| 6 | | Herman Geuvers,
Benjamin Werner:
On the Church-Rosser Property for Expressive Type Systems and its Consequences for their Metatheoretic Study
LICS 1994: 320-329 |
| 5 | | Franco Barbanera,
Maribel Fernández,
Herman Geuvers:
Modularity of Strong Normalization and Confluence in the algebraic-lambda-Cube
LICS 1994: 406-415 |
| 4 | | Herman Geuvers:
A short and flexible proof of Strong Normalization for the Calculus of Constructions.
TYPES 1994: 14-38 |
| 1993 |
|---|
| 3 | | Herman Geuvers:
Conservativity between Logics and Typed lambda Calculi.
TYPES 1993: 79-107 |
| 1992 |
|---|
| 2 | | Herman Geuvers:
The Church-Rosser Property for beta-eta-reduction in Typed lambda-Calculi
LICS 1992: 453-460 |
| 1991 |
|---|
| 1 | | Herman Geuvers,
Mark-Jan Nederhof:
Modular Proof of Strong Normalization for the Calculus of Constructions.
J. Funct. Program. 1(2): 155-189 (1991) |
