עקוב אחר
Herman Geuvers
Herman Geuvers
Radboud University Nijmegen, the Netherlands
כתובת אימייל מאומתת בדומיין cs.ru.nl - דף הבית
כותרת
צוטט על ידי
צוטט על ידי
שנה
Logics and type systems‏
JH Geuvers‏
[Sl: sn], 1993‏
2331993
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‏
1832009
Proof-assistants using dependent type systems‏
H Barendregt, H Geuvers‏
Handbook of automated reasoning 2, 1149-1238, 2001‏
1572001
Selected papers on Automath‏
RP Nederpelt, JH Geuvers, editors Roel, C De Vrijer‏
North-Holland, 1994‏
1371994
C-CoRN, the constructive Coq repository at Nijmegen‏
L Cruz-Filipe, H Geuvers, F Wiedijk‏
Mathematical Knowledge Management: Third International Conference, MKM 2004 …, 2004‏
1362004
Inductive and coinductive types with iteration and recursion‏
JH Geuvers‏
Bastad: Chalmers University of Technology, 1992‏
1361992
The Church-Rosser property for βη-reduction in typed λ-calculi‏
JH Geuvers‏
Washington: IEEE, 1992‏
991992
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
A constructive algebraic hierarchy in Coq‏
H Geuvers, R Pollack, F Wiedijk, J Zwanenburg‏
Journal of Symbolic Computation 34 (4), 271-286, 2002‏
862002
Type theory and formal proof: an introduction‏
R Nederpelt, H Geuvers‏
Cambridge University Press, 2014‏
842014
Explicit substitution on the edge of strong normalization‏
R Bloo, H Geuvers‏
Theoretical Computer Science 211 (1-2), 375-395, 1999‏
801999
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 in the algebraic-λ-cube‏
F Barbanera, M Fernández, H Geuvers‏
Journal of Functional Programming 7 (6), 613-660, 1997‏
681997
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‏
602001
Constructive reals in Coq: Axioms and categoricity‏
H Geuvers, M Niqui‏
International Workshop on Types for Proofs and Programs, 79-95, 2000‏
592000
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
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‏
441994
המערכת אינה יכולה לבצע את הפעולה כעת. נסה שוב מאוחר יותר.
מאמרים 1–20