Seguir
Herman Geuvers
Herman Geuvers
Dirección de correo verificada de cs.ru.nl - Página principal
Título
Citado por
Citado por
Año
Logics and type systems
JH Geuvers
[Sl: sn], 1993
2391993
Modular proof of strong normalization for the calculus of constructions
H Geuvers, MJ Nederhof
J. Funct. Program. 1 (2), 155-189, 1991
1891991
Proof assistants: History, ideas and future
H Geuvers
Sadhana 34, 3-25, 2009
1832009
Proof-assistants using dependent type systems
H Barendregt, H Geuvers
Handbook of automated reasoning, 1149-1238, 2001
1552001
Selected papers on Automath
RP Nederpelt, JH Geuvers, editors Roel, C De Vrijer
North-Holland, 1994
1361994
Inductive and coinductive types with iteration and recursion
JH Geuvers
Bastad: Chalmers University of Technology, 1992
1361992
C-CoRN, the constructive Coq repository at Nijmegen
L Cruz-Filipe, H Geuvers, F Wiedijk
Mathematical Knowledge Management: Third International Conference, MKM 2004 …, 2004
1352004
The Church-Rosser property for βη-reduction in typed λ-calculi
JH Geuvers
[Sl]: IEEE, 1992
1001992
Automation of higher-order logic
C Benzmüller, D Miller
Handbook of the History of Logic 9, 215-254, 2014
902014
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
881994
Type theory and formal proof: an introduction
R Nederpelt, H Geuvers
Cambridge University Press, 2014
852014
A constructive algebraic hierarchy in Coq
H Geuvers, R Pollack, F Wiedijk, J Zwanenburg
Journal of Symbolic Computation 34 (4), 271-286, 2002
842002
Explicit substitution on the edge of strong normalization
R Bloo, H Geuvers
Theoretical Computer Science 211 (1-2), 375-395, 1999
791999
Modularity of strong normalization in the algebraic-λ-cube
F Barbanera, M Fernández, H Geuvers
Journal of Functional Programming 7 (6), 613-660, 1997
701997
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
682002
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
661994
Induction is not derivable in second order dependent type theory
H Geuvers
International Conference on Typed Lambda Calculi and Applications, 166-181, 2001
592001
Constructive reals in Coq: Axioms and categoricity
H Geuvers, M Niqui
International Workshop on Types for Proofs and Programs, 79-95, 2000
592000
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
461994
Diaframe: automated verification of fine-grained concurrent programs in Iris
I Mulder, R Krebbers, H Geuvers
Proceedings of the 43rd ACM SIGPLAN International Conference on Programming …, 2022
442022
El sistema no puede realizar la operación en estos momentos. Inténtalo de nuevo más tarde.
Artículos 1–20