Follow
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
2321993
Modular proof of strong normalization for the calculus of constructions
H Geuvers, MJ Nederhof
J. Funct. Program. 1 (2), 155-189, 1991
1841991
Proof assistants: History, ideas and future
H Geuvers
Sadhana 34, 3-25, 2009
1532009
Proof-assistants using dependent type systems
H Barendregt, H Geuvers
Handbook of automated reasoning, 1149-1238, 2001
1472001
Selected papers on Automath
RP Nederpelt, JH Geuvers, editors Roel, C De Vrijer
North-Holland, 1994
1331994
Inductive and coinductive types with iteration and recursion
JH Geuvers
Bastad: Chalmers University of Technology, 1992
1311992
C-CoRN, the constructive Coq repository at Nijmegen
L Cruz-Filipe, H Geuvers, F Wiedijk
Mathematical Knowledge Management: Third International Conference, MKM 2004 …, 2004
1232004
The Church-Rosser property for βη-reduction in typed λ-calculi
JH Geuvers
[Sl]: IEEE, 1992
1001992
A short and flexible proof of strong normalization for the calculus of constructions
H Geuvers
Types for Proofs and Programs: International Workshop TYPES'94 Båstad …, 2005
862005
Automation of Higher-Order Logic.
C Benzmüller, D Miller
Computational Logic 9, 215-254, 2014
832014
A constructive algebraic hierarchy in Coq
H Geuvers, R Pollack, F Wiedijk, J Zwanenburg
Journal of Symbolic Computation 34 (4), 271-286, 2002
802002
Explicit substitution on the edge of strong normalization
R Bloo, H Geuvers
Theoretical Computer Science 211 (1-2), 375-395, 1999
801999
Type theory and formal proof: an introduction
R Nederpelt, H Geuvers
Cambridge University Press, 2014
692014
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
681994
Modularity of strong normalization in the algebraic-λ-cube
F Barbanera, M Fernández, H Geuvers
Journal of functional programming 7 (6), 613-660, 1997
671997
A constructive proof of the fundamental theorem of algebra without using the rationals
H Geuvers, F Wiedijk, J Zwanenburg
Types for Proofs and Programs: International Workshop, TYPES 2000 Durham, UK …, 2002
642002
Constructive reals in Coq: Axioms and categoricity
H Geuvers, M Niqui
Types for Proofs and Programs: International Workshop, TYPES 2000 Durham, UK …, 2002
532002
Induction is not derivable in second order dependent type theory
H Geuvers
Typed Lambda Calculi and Applications: 5th International Conference, TLCA …, 2001
472001
On the Church-Rosser property for expressive type systems and its consequences for their metatheoretic study
H Geuvers, B Werner
Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, 320-329, 1994
421994
Open proofs and open terms: A basis for interactive logic
H Geuvers, GI Jojgov
Computer Science Logic: 16th International Workshop, CSL 2002 11th Annual …, 2002
402002
The system can't perform the operation now. Try again later.
Articles 1–20