| Logics and type systems JH Geuvers [Sl: sn], 1993 | 223 | 1993 |
| 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 | 193 | 1994 |
| 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 | 187 | 2014 |
| Modular proof of strong normalization for the calculus of constructions JH Geuvers, MJ Nederhof | 174 | 1991 |
| Proof-Assistants Using Dependent Type Systems. H Barendregt, H Geuvers Handbook of automated reasoning 2, 1149-1238, 2001 | 139 | 2001 |
| Inductive and coinductive types with iteration and recursion JH Geuvers Bastad: Chalmers University of Technology, 1992 | 133 | 1992 |
| Proof assistants: History, ideas and future H Geuvers Sadhana 34 (1), 3-25, 2009 | 123 | 2009 |
| Selected papers on Automath RP Nederpelt, JH Geuvers, editors Roel, C De Vrijer North-Holland, 1994 | 111 | 1994 |
| C-CoRN, the constructive Coq repository at Nijmegen L Cruz-Filipe, H Geuvers, F Wiedijk International Conference on Mathematical Knowledge Management, 88-103, 2004 | 108 | 2004 |
| seL4 enforces integrity T Sewell, S Winwood, P Gammie, T Murray, J Andronick, G Klein International Conference on Interactive Theorem Proving, 325-340, 2011 | 99 | 2011 |
| The Church-Rosser property for βη-reduction in typed λ-calculi JH Geuvers [Sl]: IEEE, 1992 | 95 | 1992 |
| Explicit substitution on the edge of strong normalization R Bloo, H Geuvers Theoretical Computer Science 211 (1-2), 375-395, 1999 | 79 | 1999 |
| 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 | 76 | 1994 |
| A constructive algebraic hierarchy in Coq H Geuvers, R Pollack, F Wiedijk, J Zwanenburg Journal of Symbolic Computation 34 (4), 271-286, 2002 | 71 | 2002 |
| Automation of Higher-Order Logic. C Benzmüller, D Miller, H Geuvers, BW Paleo Computational Logic 9, 215-254, 2014 | 69 | 2014 |
| Modularity of strong normalization in the algebraic-λ-cube F Barbanera, M Fernández, H Geuvers Journal of functional programming 7 (6), 613-660, 1997 | 64 | 1997 |
| 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 | 63 | 1994 |
| 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 | 58 | 2000 |
| 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 | 57 | 1994 |
| Type theory and formal proof: an introduction R Nederpelt, H Geuvers Cambridge University Press, 2014 | 55 | 2014 |
Josef UrbanPrincipal Researcher at Czech Technical University in PragueVerified email at cvut.cz
