Herman Geuvers
Herman Geuvers
Verified email at cs.ru.nl - Homepage
Title
Cited by
Cited by
Year
Logics and type systems
JH Geuvers
[Sl: sn], 1993
2231993
Checking Landau's “Grundlagen” in the Automath System: Parts of Chapters 0, 1 and 2 (Introduction, Prepration, Translation)
LS van Benthem Jutting
Studies in Logic and the Foundations of Mathematics 133, 701-720, 1994
1921994
Lactobacillus-dominated cervicovaginal microbiota associated with reduced HIV/STI prevalence and genital HIV viral load in African women
H Borgdorff, E Tsivtsivadze, R Verhelst, M Marzorati, S Jurriaans, ...
The ISME journal 8 (9), 1781-1793, 2014
1842014
Modular proof of strong normalization for the calculus of constructions
JH Geuvers, MJ Nederhof
1741991
Proof-Assistants Using Dependent Type Systems.
H Barendregt, H Geuvers
Handbook of automated reasoning 2, 1149-1238, 2001
1382001
Inductive and coinductive types with iteration and recursion
JH Geuvers
Bastad: Chalmers University of Technology, 1992
1331992
Proof assistants: History, ideas and future
H Geuvers
Sadhana 34 (1), 3-25, 2009
1232009
Selected papers on Automath
RP Nederpelt, JH Geuvers, editors Roel, C De Vrijer
North-Holland, 1994
1111994
C-CoRN, the constructive Coq repository at Nijmegen
L Cruz-Filipe, H Geuvers, F Wiedijk
International Conference on Mathematical Knowledge Management, 88-103, 2004
1052004
seL4 enforces integrity
T Sewell, S Winwood, P Gammie, T Murray, J Andronick, G Klein
International Conference on Interactive Theorem Proving, 325-340, 2011
982011
The Church-Rosser property for βη-reduction in typed λ-calculi
JH Geuvers
[Sl]: IEEE, 1992
951992
Explicit substitution on the edge of strong normalization
R Bloo, H Geuvers
Theoretical Computer Science 211 (1-2), 375-395, 1999
791999
A short and flexible proof of strong normalization for the calculus of constructions
H Geuvers
International Workshop on Types for Proofs and Programs, 14-38, 1994
761994
A constructive algebraic hierarchy in Coq
H Geuvers, R Pollack, F Wiedijk, J Zwanenburg
Journal of Symbolic Computation 34 (4), 271-286, 2002
712002
Automation of Higher-Order Logic.
C Benzmüller, D Miller, H Geuvers, BW Paleo
Computational Logic 9, 215-254, 2014
692014
Modularity of strong normalization in the algebraic-λ-cube
F Barbanera, M Fernández, H Geuvers
Journal of functional programming 7 (6), 613-660, 1997
641997
Modularity of strong normalization and confluence in the algebraic-/spl lambda/-cube
F Barbanera, M Fernández, H Geuvers
Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, 406-415, 1994
631994
A constructive proof of the Fundamental Theorem of Algebra without using the rationals
H Geuvers, F Wiedijk, J Zwanenburg
International Workshop on Types for Proofs and Programs, 96-111, 2000
582000
Generalizing Automath by means of a lambda-typed lambda calculus
NG de Bruijn
Studies in Logic and the Foundations of Mathematics 133, 313-337, 1994
571994
Type theory and formal proof: an introduction
R Nederpelt, H Geuvers
Cambridge University Press, 2014
532014
The system can't perform the operation now. Try again later.
Articles 1–20