Herman Geuvers

101 papers A* 5A 1B 16C 3Journal 37Unranked 33

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Cellular Automaton Reducibility as a Measure of Complexity for Infinite Words. CoRR Markel Zubia, Herman Geuvers
2026	J	`jnl`	Non-Derivability Results in Polymorphic Dependent Type Theory. CoRR Herman Geuvers
2025	B	`conf`	Impredicative Encodings of Inductive and Coinductive Types. FSCD Steven Bronsveld, Herman Geuvers, Niels van der Weide
2025	B	`conf`	Initial Algebras of Domains via Quotient Inductive-Inductive Types. MFPS Simcha van Collem, Niels van der Weide, Herman Geuvers
2025	J	`jnl`	Master Thesis Impredicative Encodings of Inductive and Coinductive Types. CoRR Steven Bronsveld, Herman Geuvers, Niels van der Weide
2025	J	`jnl`	Positive Hennessy-Milner Logic for Branching Bisimulation. Log. Methods Comput. Sci. Herman Geuvers, Komi Golov
2024	J	`jnl`	Hashing Modulo Context-Sensitive α-Equivalence. CoRR Lasse Blaauwbroek, Miroslav Olsák, Herman Geuvers
2024	J	`jnl`	Hashing Modulo Context-Sensitive 𝛼-Equivalence. Proc. ACM Program. Lang. Lasse Blaauwbroek, Miroslav Olsák, Herman Geuvers
2022	—	`conf`	Apartness and Distinguishing Formulas in Hennessy-Milner Logic. A Journey from Process Algebra via Timed Automata to Model Learning Herman Geuvers
2022	J	`jnl`	Characteristics of de Bruijn's early proof checker Automath. CoRR Herman Geuvers, Rob Nederpelt
2022	J	`jnl`	Characteristics of de Bruijn's early proof checker Automath. Fundam. Informaticae Herman Geuvers, Rob Nederpelt
2022	—	`conf`	Classical Natural Deduction from Truth Tables. TYPES Herman Geuvers, Tonny Hurkens
2022	A*	`conf`	Diaframe: automated verification of fine-grained concurrent programs in Iris. PLDI Ike Mulder, Robbert Krebbers, Herman Geuvers
2022	J	`jnl`	Directed branching bisimulation via apartness and positive logic. CoRR Herman Geuvers, Anton Golov
2021	J	`jnl`	Relating Apartness and Bisimulation. Log. Methods Comput. Sci. Herman Geuvers, Bart Jacobs
2020	J	`jnl`	Relating Apartness and Bisimulation. CoRR Herman Geuvers, Bart Jacobs
2020	B	`conf`	Tactic Learning and Proving for the Coq Proof Assistant. LPAR Lasse Blaauwbroek, Josef Urban, Herman Geuvers
2020	J	`jnl`	Tactic Learning and Proving for the Coq Proof Assistant. CoRR Lasse Blaauwbroek, Josef Urban, Herman Geuvers
2020	J	`jnl`	The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq. CoRR Lasse Blaauwbroek, Josef Urban, Herman Geuvers
2020	C	`conf`	The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq. CICM Lasse Blaauwbroek, Josef Urban, Herman Geuvers
2019	B	`ed.`	4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, Dortmund, Germany, June 24-30, 2019 FSCD Herman Geuvers
2019	J	`jnl`	A benchmark for C program verification. CoRR Marko C. J. D. van Eekelen, Daniil Frumin, Herman Geuvers, Léon Gondelman, Robbert Krebbers, Marc Schoolderman, Sjaak Smetsers, Freek Verbeek, Benoît Viguier, Freek Wiedijk
2019	J	`jnl`	Strong Normalization for Truth Table Natural Deduction. Fundam. Informaticae Herman Geuvers, Iris van der Giessen, Tonny Hurkens
2019	B	`conf`	The Construction of Set-Truncated Higher Inductive Types. MFPS Niels van der Weide, Herman Geuvers
2018	—	`ed.`	22nd International Conference on Types for Proofs and Programs, TYPES 2016, Novi Sad, Serbia, May 23-26, 2016 TYPES Silvia Ghilezan, Herman Geuvers, Jelena Ivetic
2018	B	`conf`	Finite sets in homotopy type theory. CPP Dan Frumin, Herman Geuvers, Léon Gondelman, Niels van der Weide
2017	B	`conf`	A Formalisation of Consistent Consequence for Boolean Equation Systems. ITP Myrthe van Delft, Herman Geuvers, Tim A. C. Willemse
2017	—	`conf`	Deriving Natural Deduction Rules from Truth Tables. ICLA Herman Geuvers, Tonny Hurkens
2017	J	`jnl`	Higher Inductive Types in Programming. J. Univers. Comput. Sci. Henning Basold, Herman Geuvers, Niels van der Weide
2017	C	`ed.`	Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings CICM Herman Geuvers, Matthew England, Osman Hasan, Florian Rabe, Olaf Teschke
2017	—	`conf`	Proof Terms for Generalized Natural Deduction. TYPES Herman Geuvers, Tonny Hurkens
2016	A*	`conf`	Type Theory based on Dependent Inductive and Coinductive Types. LICS Henning Basold, Herman Geuvers
2016	J	`jnl`	Type Theory based on Dependent Inductive and Coinductive Types. CoRR Henning Basold, Herman Geuvers
2014	—	`conf`	A type system for Continuation Calculus. CL&C Herman Geuvers, Wouter Geraedts, Bram Geron, Judith van Stegeren
2014	C	`conf`	Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description. CICM Cezary Kaliszyk, Josef Urban, Jirí Vyskocil, Herman Geuvers
2014	J	`jnl`	Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Description. CoRR Cezary Kaliszyk, Josef Urban, Jirí Vyskocil, Herman Geuvers
2013	B	`conf`	Communicating Formal Proofs: The Case of Flyspeck. ITP Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers
2013	—	`conf`	Continuation calculus. COS Bram Geron, Herman Geuvers
2013	—	`conf`	Explicit convertibility proofs in pure type systems. LFMTP Floris van Doorn, Herman Geuvers, Freek Wiedijk
2013	J	`jnl`	Formal Mathematics on Display: A Wiki for Flyspeck CoRR Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers
2013	—	`conf`	Formal Mathematics on Display: A Wiki for Flyspeck. MKM/Calculemus/DML Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers
2013	J	`jnl`	The Ann. Pure Appl. Log. Herman Geuvers, Robbert Krebbers, James McKinna
2012	—	`ed.`	Proceedings Fourth Workshop on Classical Logic and Computation, CL&C 2012, Warwick, England, 8th July 2012. CL&C Herman Geuvers, Ugo de'Liguoro
2012	J	`jnl`	The lambda-mu-T-calculus CoRR Herman Geuvers, Robbert Krebbers, James McKinna
2011	B	`ed.`	Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings ITP Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, Freek Wiedijk
2011	—	`conf`	Learning2Reason. Calculemus/MKM Daniel Kühlwein, Josef Urban, Evgeni Tsivtsivadze, Herman Geuvers, Tom Heskes
2011	J	`jnl`	Levels of undecidability in rewriting. Inf. Comput. Jörg Endrullis, Herman Geuvers, Jakob Grue Simonsen, Hans Zantema
2011	—	`conf`	Multi-output Ranking for Automated Reasoning. KDIR Daniel Kühlwein, Josef Urban, Evgeni Tsivtsivadze, Herman Geuvers, Tom Heskes
2011	—	`ed.`	Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2011, Nijmegen, The Netherlands, August 26, 2011. LFMTP Herman Geuvers, Gopalan Nadathur
2011	A	`conf`	Semantic Graph Kernels for Automated Reasoning. SDM Evgeni Tsivtsivadze, Josef Urban, Herman Geuvers, Tom Heskes
2011	J	`jnl`	The correctness of Newman's typability algorithm and some of its extensions. Theor. Comput. Sci. Herman Geuvers, Robbert Krebbers
2010	J	`jnl`	A Wiki for Mizar: Motivation, Considerations, and Initial Prototype CoRR Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers
2010	—	`conf`	A Wiki for Mizar: Motivation, Considerations, and Initial Prototype. AISC/MKM/Calculemus Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers
2010	B	`conf`	Automated Machine-Checked Hybrid System Safety Proofs. ITP Herman Geuvers, Adam Koprowski, Dan Synek, Eelis van der Weegen
2010	—	`conf`	Narrating Formal Proof (Work in Progress). UITP Carst Tankink, Herman Geuvers, James McKinna
2010	J	`jnl`	Proviola: A Tool for Proof Re-animation CoRR Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk
2010	—	`conf`	Proviola: A Tool for Proof Re-animation. AISC/MKM/Calculemus Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk
2010	—	`conf`	Pure Type Systems without Explicit Contexts LFMTP Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk
2009	—	`conf`	A Logically Saturated Extension of lambdaµµ. Calculemus/MKM Lionel Elie Mamane, Herman Geuvers, James McKinna
2009	J	`jnl`	Degrees of Undecidability in Rewriting CoRR Jörg Endrullis, Herman Geuvers, Hans Zantema
2009	B	`conf`	Degrees of Undecidability in Term Rewriting. CSL Jörg Endrullis, Herman Geuvers, Hans Zantema
2009	J	`jnl`	Social processes, program verification and all that. Math. Struct. Comput. Sci. Andrea Asperti, Herman Geuvers, Raja Natarajan
2008	—	`conf`	A Real Semantic Web for Mathematics Deserves a Real Semantics. SemWiki Cezary Kaliszyk, Pierre Corbineau, Freek Wiedijk, James McKinna, Herman Geuvers
2008	—	`conf`	Introduction to Type Theory. LerNet ALFA Summer School Herman Geuvers
2008	J	`jnl`	Preface. Ann. Pure Appl. Log. S. Barry Cooper, Herman Geuvers, Anand Pillay, Jouko A. Väänänen
2007	J	`jnl`	Constructive analysis, types and exact real numbers. Math. Struct. Comput. Sci. Herman Geuvers, Milad Niqui, Bas Spitters, Freek Wiedijk
2007	—	`conf`	Deduction Graphs with Universal Quantification. TERMGRAPH@ETAPS Herman Geuvers, Iris Loeb
2007	J	`jnl`	Natural deduction via graphs: formal definition and computation rules. Math. Struct. Comput. Sci. Herman Geuvers, Iris Loeb
2007	J	`jnl`	Preface to the special issue: Constructive analysis, types and exact real numbers. Math. Struct. Comput. Sci. Bas Spitters, Herman Geuvers, Milad Niqui, Freek Wiedijk
2006	—	`conf`	(In)consistency of Extensions of Higher Order Logic and Type Theory. TYPES Herman Geuvers
2006	B	`conf`	From Deduction Graphs to Proof Nets: Boxes and Sharing in the Graphical Presentation of Deductions. MFCS Herman Geuvers, Iris Loeb
2005	—	`conf`	An Interactive Algebra Course with Formalised Proofs and Definitions. MKM Andrea Asperti, Herman Geuvers, Iris Loeb, Lionel Elie Mamane, Claudio Sacerdoti Coen
2004	—	`conf`	A Logical Framework with Explicit Conversions. LFM@IJCAR Herman Geuvers, Freek Wiedijk
2004	—	`conf`	C-CoRN, the Constructive Coq Repository at Nijmegen. MKM Luís Cruz-Filipe, Herman Geuvers, Freek Wiedijk
2004	—	`conf`	Rewriting for Fitch Style Natural Deductions. RTA Herman Geuvers, Rob Nederpelt
2003	—	`conf`	A Calculus of Tactics and Its Operational Semantics. MKM Symposium Gueorgui I. Jojgov, Herman Geuvers
2003	—	`ed.`	Mathematics, Logic and Computation, Satellite Event of ICALP 2003, Eindhoven, The Netherlands, July 4-5, 2003 Mathematics, Logic and Computation @ ICALP Herman Geuvers, Fairouz Kamareddine
2003	—	`conf`	Preface. Mathematics, Logic and Computation @ ICALP Herman Geuvers, Fairouz Kamareddine
2003	—	`ed.`	Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers TYPES Herman Geuvers, Freek Wiedijk
2002	J	`jnl`	A Constructive Algebraic Hierarchy in Coq. J. Symb. Comput. Herman Geuvers, Randy Pollack, Freek Wiedijk, Jan Zwanenburg
2002	B	`conf`	Open Proofs and Open Terms: A Basis for Interactive Logic. CSL Herman Geuvers, Gueorgui I. Jojgov
2002	J	`jnl`	Proof by computation in the Coq system. Theor. Comput. Sci. Martijn Oostdijk, Herman Geuvers
2001	—	`conf`	Induction Is Not Derivable in Second Order Dependent Type Theory. TLCA Herman Geuvers
2001	—	`ch.`	Proof-Assistants Using Dependent Type Systems. Handbook of Automated Reasoning Henk Barendregt, Herman Geuvers
2000	—	`conf`	A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals. TYPES Herman Geuvers, Freek Wiedijk, Jan Zwanenburg
2000	—	`conf`	Constructive Reals in Coq: Axioms and Categoricity. TYPES Herman Geuvers, Milad Niqui
2000	—	`conf`	Equational Reasoning via Partial Reflection. TPHOLs Herman Geuvers, Freek Wiedijk, Jan Zwanenburg
1999	J	`jnl`	Explicit Substitution On the Edge of Strong Normalization. Theor. Comput. Sci. Roel Bloo, Herman Geuvers
1999	B	`conf`	Safe Proof Checking in Type Theory with Y. CSL Herman Geuvers, Erik Poll, Jan Zwanenburg
1999	J	`jnl`	Some logical and syntactical observations concerning the first-order dependent type system lambda-P. Math. Struct. Comput. Sci. Herman Geuvers, Erik Barendsen
1997	J	`jnl`	Modularity of Strong Normalization in the Algebraic-lambda-Cube. J. Funct. Program. Franco Barbanera, Maribel Fernández, Herman Geuvers
1996	B	`conf`	Extending Models of Second Order Predicate Logic to Models of Second Dependent Type Theory. CSL Herman Geuvers
1995	—	`conf`	A Simple Model Construction for the Calculus of Constructions. TYPES Milena Stefanova, Herman Geuvers
1995	B	`conf`	Congruence Types. CSL Gilles Barthe, Herman Geuvers
1995	—	`conf`	Modular Properties of Algebraic Type Systems. HOA Gilles Barthe, Herman Geuvers
1994	—	`conf`	A short and flexible proof of Strong Normalization for the Calculus of Constructions. TYPES Herman Geuvers
1994	A*	`conf`	Modularity of Strong Normalization and Confluence in the algebraic-lambda-Cube LICS Franco Barbanera, Maribel Fernández, Herman Geuvers
1994	A*	`conf`	On the Church-Rosser Property for Expressive Type Systems and its Consequences for their Metatheoretic Study LICS Herman Geuvers, Benjamin Werner
1993	—	`conf`	Conservativity between Logics and Typed lambda Calculi. TYPES Herman Geuvers
1992	A*	`conf`	The Church-Rosser Property for beta-eta-reduction in Typed lambda-Calculi LICS Herman Geuvers
1991	J	`jnl`	Modular Proof of Strong Normalization for the Calculus of Constructions. J. Funct. Program. Herman Geuvers, Mark-Jan Nederhof