| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Herman Geuvers, Robbert Krebbers, James McKinna |
The lambda-mu-T-calculus  |
CoRR  |
2012 |
DBLP BibTeX RDF |
|
| 1 | Herman Geuvers, Robbert Krebbers |
The correctness of Newman's typability algorithm and some of its extensions. |
Theor. Comput. Sci. |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jörg Endrullis, Herman Geuvers, Jakob Grue Simonsen, Hans Zantema |
Levels of undecidability in rewriting. |
Inf. Comput. |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers, Gopalan Nadathur (eds.) |
Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice |
LFMTP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kühlwein, Josef Urban, Evgeni Tsivtsivadze, Herman Geuvers, Tom Heskes |
Multi-output Ranking for Automated Reasoning. |
KDIR |
2011 |
DBLP BibTeX RDF |
|
| 1 | Evgeni Tsivtsivadze, Josef Urban, Herman Geuvers, Tom Heskes |
Semantic Graph Kernels for Automated Reasoning. |
SDM |
2011 |
DBLP BibTeX RDF |
|
| 1 | Daniel Kühlwein, Josef Urban, Evgeni Tsivtsivadze, Herman Geuvers, Tom Heskes |
Learning2Reason. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk |
Proviola: A Tool for Proof Re-animation |
CoRR |
2010 |
DBLP BibTeX RDF |
|
| 1 | Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers |
A Wiki for Mizar: Motivation, Considerations, and Initial Prototype |
CoRR |
2010 |
DBLP BibTeX RDF |
|
| 1 | Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk |
Pure Type Systems without Explicit Contexts |
LFMTP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers, Adam Koprowski, Dan Synek, Eelis van der Weegen |
Automated Machine-Checked Hybrid System Safety Proofs. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers |
A Wiki for Mizar: Motivation, Considerations, and Initial Prototype. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk |
Proviola: A Tool for Proof Re-animation. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrea Asperti, Herman Geuvers, Raja Natarajan |
Social processes, program verification and all that. |
Mathematical Structures in Computer Science |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Jörg Endrullis, Herman Geuvers, Hans Zantema |
Degrees of Undecidability in Rewriting |
CoRR |
2009 |
DBLP BibTeX RDF |
|
| 1 | Lionel Elie Mamane, Herman Geuvers, James McKinna |
A Logically Saturated Extension of lambdaµµ. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Jörg Endrullis, Herman Geuvers, Hans Zantema |
Degrees of Undecidability in Term Rewriting. |
CSL |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers, Freek Wiedijk |
A Logical Framework with Explicit Conversions. |
Electr. Notes Theor. Comput. Sci. |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers, Iris Loeb |
Deduction Graphs with Universal Quantification. |
Electr. Notes Theor. Comput. Sci. |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | S. Barry Cooper, Herman Geuvers, Anand Pillay, Jouko A. Väänänen |
Preface. |
Ann. Pure Appl. Logic |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Cezary Kaliszyk, Pierre Corbineau, Freek Wiedijk, James McKinna, Herman Geuvers |
A Real Semantic Web for Mathematics Deserves a Real Semantics. |
SemWiki |
2008 |
DBLP BibTeX RDF |
|
| 1 | Herman Geuvers |
Introduction to Type Theory. |
LerNet ALFA Summer School |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers, Iris Loeb |
Natural deduction via graphs: formal definition and computation rules. |
Mathematical Structures in Computer Science |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers, Milad Niqui, Bas Spitters, Freek Wiedijk |
Constructive analysis, types and exact real numbers. |
Mathematical Structures in Computer Science |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers, Iris Loeb |
From Deduction Graphs to Proof Nets: Boxes and Sharing in the Graphical Presentation of Deductions. |
MFCS |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers |
(In)consistency of Extensions of Higher Order Logic and Type Theory. |
TYPES |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrea Asperti, Herman Geuvers, Iris Loeb, Lionel Elie Mamane, Claudio Sacerdoti Coen |
An Interactive Algebra Course with Formalised Proofs and Definitions. |
MKM |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Gueorgui I. Jojgov, Herman Geuvers |
A Calculus of Tactics and Its Operational Semantics. |
Electr. Notes Theor. Comput. Sci. |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Luís Cruz-Filipe, Herman Geuvers, Freek Wiedijk |
C-CoRN, the Constructive Coq Repository at Nijmegen. |
MKM |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers, Rob Nederpelt |
Rewriting for Fitch Style Natural Deductions. |
RTA |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers, Fairouz Kamareddine |
Preface. |
Electr. Notes Theor. Comput. Sci. |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
TYPES |
2003 |
DBLP BibTeX RDF |
|
| 1 | Martijn Oostdijk, Herman Geuvers |
Proof by computation in the Coq system. |
Theor. Comput. Sci. |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers, Randy Pollack, Freek Wiedijk, Jan Zwanenburg |
A Constructive Algebraic Hierarchy in Coq. |
J. Symb. Comput. |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers, Gueorgui I. Jojgov |
Open Proofs and Open Terms: A Basis for Interactive Logic. |
CSL |
2002 |
DBLP DOI BibTeX RDF |
open terms, meta-variables, formulas-as-types, type theory, interactive theorem proving |
| 1 | Henk Barendregt, Herman Geuvers |
Proof-Assistants Using Dependent Type Systems. |
Handbook of Automated Reasoning |
2001 |
DBLP BibTeX RDF |
|
| 1 | Herman Geuvers |
Induction Is Not Derivable in Second Order Dependent Type Theory. |
TLCA |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers, Milad Niqui |
Constructive Reals in Coq: Axioms and Categoricity. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers, Freek Wiedijk, Jan Zwanenburg |
A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers, Freek Wiedijk, Jan Zwanenburg |
Equational Reasoning via Partial Reflection. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Roel Bloo, Herman Geuvers |
Explicit Substitution On the Edge of Strong Normalization. |
Theor. Comput. Sci. |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers, Erik Barendsen |
Some logical and syntactical observations concerning the first-order dependent type system lambda-P. |
Mathematical Structures in Computer Science |
1999 |
DBLP BibTeX RDF |
|
| 1 | Herman Geuvers, Erik Poll, Jan Zwanenburg |
Safe Proof Checking in Type Theory with Y. |
CSL |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Franco Barbanera, Maribel Fernández, Herman Geuvers |
Modularity of Strong Normalization in the Algebraic-lambda-Cube. |
J. Funct. Program. |
1997 |
DBLP BibTeX RDF |
|
| 1 | Herman Geuvers |
Extending Models of Second Order Predicate Logic to Models of Second Dependent Type Theory. |
CSL |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Milena Stefanova, Herman Geuvers |
A Simple Model Construction for the Calculus of Constructions. |
TYPES |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Herman Geuvers |
Modular Properties of Algebraic Type Systems. |
HOA |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Herman Geuvers |
Congruence Types. |
CSL |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers |
A short and flexible proof of Strong Normalization for the Calculus of Constructions. |
TYPES |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers, Benjamin Werner |
On the Church-Rosser Property for Expressive Type Systems and its Consequences for their Metatheoretic Study |
LICS |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Franco Barbanera, Maribel Fernández, Herman Geuvers |
Modularity of Strong Normalization and Confluence in the algebraic-lambda-Cube |
LICS |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers |
Conservativity between Logics and Typed lambda Calculi. |
TYPES |
1993 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers |
The Church-Rosser Property for beta-eta-reduction in Typed lambda-Calculi |
LICS |
1992 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers, Mark-Jan Nederhof |
Modular Proof of Strong Normalization for the Calculus of Constructions. |
J. Funct. Program. |
1991 |
DBLP BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")