Publications of Herman Geuvers
2017
2016
 Freek Wiedijk, Herman Geuvers, Josef Urban
Een
wiskundig bewijs correct bewezen: De meest efficiente manier om bollen
op te stapelen (in Dutch), Nieuw Archief voor Wiskunde (NAW) 5/17
nr.3 september 2016, pp. 177183.
 Henning Basold, Herman Geuvers, Niels van der Weide
Higher Inductive Types in Programming, submitted
 Henning Basold, Herman Geuvers
Type Theory
based on Dependent Inductive and Coinductive Types,
LICS 2016.
 Herman Geuvers and Tonny Hurkens
Deriving natural deduction rules
from truth tables (Extended version).
 Herman Geuvers
Inductive and Coinductive types with Iteration and Recursion in a
Polymorphic Framework (1992). This is an extended version, with some
obervations on using Sigma types tot do dependent induction/recursion,
of the (also never formally pubished)
Inductive
and Coinductive Types with Iteration and Recursion, which appeared
in the informal proceedings of the 1992 workshop on Types for Proofs
and Programs, Bastad 1992, Sweden, eds. B. Nordstrom, K. Petersson and
G. Plotkin, pp 183207.
2015
2014
 Rob Nederpelt and Herman Geuvers
Type Theory and Formal Proof, An
Introduction, Cambridge University Press, December 2014.
 Herman Geuvers
Properties
of a lambda calculus with definitions, Short note, providing
some proofs that were omitted in the book Type Theory and
Formal Proof, An Introduction, covering the metatheory of the
system with definitions.

Herman Geuvers, Wouter Geraedts, Bram Geron, Judith van Stegeren
A type
system for Continuation Calculus, EPTCS 164 Proceedings Fifth
International Workshop on Classical Logic and Computation Vienna,
Austria, July 13, 2014 Ed. Paulo Oliva, pp. 118.
 Cezary Kaliszyk, Josef Urban, Jiri Vyskocil, Herman Geuvers
Developing CorpusBased Translation Methods between Informal and
Formal Mathematics: Project Description. CICM 2014, LNCS 8543,
Springer, pp. 435439.
2013

H. Geuvers
R. Nederpelt,
N.G. de
Bruijn's Contribution to the Formalization of Mathematics, , Indagationes Mathematicae Volume 24, Issue 4, 15 November 2013, Pages 10341049, In memory of N.G. (Dick) de Bruijn (19182012),
Science Direct.
 H. Geuvers,
Inconsistency of "Automath powersets" in impredicative type
theory, Short note, November 2013.
 B. Geron and H. Geuvers,
Continuation calculus, in Proceedings of the First Workshop on
Control Operators and their Semantics (COS),
Eindhoven, The Netherlands, June 2425, 2013
Eds. Ugo de'Liguoro and Alexis Saurin, EPTCS 127.
 F. van Doorn, H. Geuvers F. Wiedijk, Explicit Convertibility
Proofs in Pure Type
Systems, in
Proceedings of LFMTP 2013, the Eighth ACM SIGPLAN international workshop on Logical frameworks and metalanguages: theory and practice, Boston USA, September 2013, ACM (digital library).
 H. Geuvers, R. Krebbers and J. McKinna,
The
lambdamuTcalculus. In volume
164, issue 6 of APAL, pages
676701. [pdf] [at
publisher]
 C. Tankink, C. Kaliszyk, J. Urban and H. Geuvers
Formal Mathematics on Display:
A Wiki for Flyspeck, in the proceedings of
CICM 2013, Bath UK, July 2013.
 C. Tankink, C. Kaliszyk, J. Urban and H. Geuvers
Communicating
Formal Proofs: The Case of Flyspeck , in the proceedings
of ITP 2013, Rennes, France, July 2013.
2012
 C. Tankink, H. Geuvers, J. McKinna: Narrating Formal Proof. Electr. Notes Theor. Comput. Sci. 285: 7183 (2012)

H. Geuvers, U. de'Liguoro (Eds.): Proceedings Fourth Workshop on Classical Logic and Computation. EPTCS 97, 2012
2011
 E. Tsivtsivadze, J. Urban, H. Geuvers, T. Heskes,
Semantic
Graph Kernels for Automated Reasoning. Proceedings of the Eleventh
SIAM International Conference on Data Mining, SDM 2011, Mesa, Arizona,
USA, SIAM/Omnipress, pp. 795803
 H. Geuvers, R. Krebbers,
The correctness of Newman's typability algorithm and some of its extensions. Theor. Comput. Sci. 412(28): 32423261 (2011)
 J. Endrullis, H. Geuvers, J. G. Simonsen and H. Zantema,
Levels of Undecidability in Rewriting.
In: Information and Computation 209 (2). 2011. pp. 227245.
 H. Geuvers, G. Nadathur (editors)
Proceedings Sixth
International Workshop on Logical Frameworks and Metalanguages:
Theory and Practice LFMTP 2011, EPTCS 71.
 Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz,
Freek Wiedijk (editors)
Interactive Theorem Proving  Second
International Conference, ITP 2011, Berg en Dal, The Netherlands,
August 2225, 2011. Proceedings LNCS 6898, Springer 2011
 Daniel Kuehlwein, Josef Urban, Evgeni Tsivtsivadze, Herman
Geuvers, Tom Heskes
Learning2Reason. Proceedings of Calculemus/MKM
2011, Springer LNCS 6824, pp. 298300
 Daniel Kuehlwein, Josef Urban, Evgeni Tsivtsivadze, Herman
Geuvers, Tom Heskes
Multioutput Ranking for Automated
Reasoning. KDIR 2011  Proceedings of the International Conference on
Knowledge Discovery and Information Retrieval, Paris, France, 2629
October, 2011. SciTePress 2011, pp. 4251
2010
 H. Geuvers, A. Koprowski, D. Synek and E. van der Weegen
Automated MachineChecked Hybrid System Safety Proofs. In
LNCS 6172, eds. M. Kaufmann and L. Paulson, conference on Interactive Theorem Proving, Edinburgh UK, pp. 259274, Springer.
 C. Tankink, H. Geuvers, J. McKinna and F. Wiedijk,
Proviola:
a Tool for Proof Reanimation, Conference on Intelligent Computer
Mathematics (CICM), Paris. LNCS 6167,2010, pp. 440454, Springer.preprint.
 J. Urban, J. Alama, P. Rudnicki and H. Geuvers,
A Wiki for Mizar: Motivation, Considerations, and Initial Prototype,
Conference on Intelligent Computer
Mathematics (CICM), Paris. LNCS 6167,2010, pp. 455469, Springer.preprint.
 C. Tankink, H. Geuvers and J. McKinna,
Narrating
Formal Proof (Work in Progress), proceedings of 9th International
Workshop on User Interfaces for Theorem Provers (UITP), associated
with IJCAR and ITP FLoC, Edinburgh UK.
 H. Geuvers, R. Krebbers, J. McKinna and F. Wiedijk,
Pure Type Systems
without Explicit Contexts, Karl Crary, Marino Miculan (Eds.): Proceedings 5th International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP). EPTCS 34 2010, pages 5367.
2009
 A. Asperti, H. Geuvers and N. Raja,
Social processes, program verification and all that, Math. Struct. in Comp. Science, vol. 19, pp. 877896, Cambridge University Press 2009.
 S. Barry Cooper, Herman Geuvers, Anand Pillay and Jouko
A. Väänänen (Eds.),
Logic Colloquium 2006 Series: Lecture
Notes in Logic (Association for Symbolic Logic), Cambridge University
Press 384 pp. 2009.
 Joerg Endrullis, Herman Geuvers and Hans Zantema,
Degrees of Undecidability in Term Rewriting,
In Proc. Conf. on Computer Science Logic (CSL '09), E. Grädel and R. Kahle (Eds.), LNCS 5771, pp. 255270, Springer, 2009.
 H. Geuvers
Proof Assistants: history, ideas and future
, in
Sadhana Journal, Academy Proceedings in Engineering Sciences,
Special Issue on Interactive Theorem Proving and Proof Checking,
Indian Academy of Sciences, Vol 34, part 1, February 2009, pp 325.

L. Mamane, H. Geuvers, J. McKinna, A Logically Saturated
Extension of lambdabarmumutilde, in Proceedings
of 8th International Conference MKM, Grand Bend, Canada, July
612, 2009, eds. J. Carette, L. Dixon, C. Sacerdoti Coen,
S. Watt, volume 5625 of Lecture Notes in Computer Science, Springer
Verlag, pages 405  421
 L. Mamane, H. Geuvers, J. McKinna, A Saturated Extension of
lambdabarmumutilde. Technical Report, Radboud
University Nijmegen. ICISR09002. July 2009.

H. Geuvers
Introduction
to Type Theory , in Language Engineering and Rigourous
Software Development (Revised Tutorial Lecture Notes
of LerNet ALFA Summer
School Piriapolis, Uruguay, 24 February to 1 March, 2008), eds.: Ana
Bove, Luis Soares Barbosa, Alberto Pardo, Jorge Sousa Pinto, LNCS
5520, Springer 2009. This is an improved version, with some small mistakes repaired.
 H. Geuvers and J. Verkoelen,
On Fixed point and Looping Combinators in Type Theory, note.
2008
 S. Barry Cooper, Herman Geuvers, Anand Pillay and Jouko A. Väänänen (eds.),
Preface, Special issue of selected papers from Logic Colloquium 2006,
Ann. Pure Appl. Logic, vol 156, nr. 1 pages 12, 2008
 H. Geuvers, F. Wiedijk
A logical framework with explicit
conversions. In: Carsten Schürmann (ed.), Proceedings of the Fourth
International Workshop on Logical Frameworks and MetaLanguages, Cork,
Ireland, Electronic Notes in
Theoretical Computer Science, Volume 199, 24 February 2008, Pages 3347.
 H. Geuvers and I. Loeb
Deduction
Graphs with Universal Quantification, I. Mackie and D. Plump
(Eds): Proceedings of TERMGRAPH 2007,
Electronic Notes in
Theoretical Computer Science, Volume 203, Issue 1, 28 March 2008, Pages 93108.
 Pierre Corbineau, Herman Geuvers, Cezary Kaliszyk, James McKinna, Freek Wiedijk
A real Semantic Web for mathematics deserves a real semantics
Proceedings of the 3rd Semantic Wiki Workshop (SemWiki 2008) at the 5th European Semantic Web Conference (ESWC 2008), Tenerife, Spain, June 2008,
Eds. C. Lange, S. Schaffert,H. SkafMolli, M. Völkel, CEUR Workshop Proceedings ISSN 16130073, vol 360.
2007
 H. Geuvers, I. Loeb
Natural Deduction via Graphs: Formal Definition and Computation Rules
Mathematical Structures in Computer Science (Special Issue on Theory and Applications of Term Graph Rewriting),
Volume 17, Issue 03, pp 485526, 2007.
 Herman Geuvers, Milad Niqui, Bas Spitters, Freek Wiedijk
Constructive analysis, types and exact real numbers
Mathematical
Structures in Computer Science, Volume 17, Issue 01, pp 336, 2007.
 Bas Spitters, Herman Geuvers, Milad Niqui, Freek Wiedijk
editors,
MSCS special issue: Constructive analysis, types and exact real numbers
Mathematical Structures in Computer Science, Volume 17, Issue 01, 2007.
 H. Geuvers
(In)consistency of extensions of Higher Order Logic and Type
Theory
In: Types for Proofs and Programs, International
Workshop, TYPES 2006, Nottingham, UK, April 1821, 2006, Revised
Selected Papers. Edited by Thorsten Altenkirch and Conor McBride.
LNCS 4502, 2007. pp. 140159.
 H. Geuvers
Computerondersteund redeneren: de boekhouder steunt de denker (Dutch)
inaugural speech , Radboud University Nijmegen, March 9 2007, ISBN 9789090216874.
 H. Geuvers
Computerondersteund redeneren: de boekhouder steunt de denker (Dutch)
short version of my inaugural speech, Automatisering Gids
nr. 10, page 15, March 9 2007.
 H. Geuvers, E. Poll
Iteration and Primitive Recursion in Categorical Terms
In: Reflections on Type Theory, Lambda Calculus, and the Mind, Essays Dedicated to Henk Barendregt on the Occasion of his 60th Birthday.
Edited by E. Barendsen, H. Geuvers, V. Capretta, M. Niqui .
Radboud Universiteit Nijmegen.
2007, pp. 101  114.
 E. Barendsen, H. Geuvers, V. Capretta, M. Niqui (editors)
Reflections on Type Theory, Lambda Calculus, and the Mind,
Essays Dedicated to Henk Barendregt on the Occasion of his 60th Birthday
December 20, Radboud Universiteit Nijmegen.
2007, see the symposium web page.
2006
 A. Asperti, H. Geuvers, I. Loeb, L. Mamane and C. Sacerdoti
Coen
An Interactive Algebra Course with Formalised Proofs and Definitions
Proceedings of the Fourth Conference Mathematical Knowledge Management,
ed. M. Kohlhase, Lecture Notes in Artificial Intelligence 3863,
Springer, 2006, pp. 315329.
 H. Geuvers, I. Loeb
From Deduction Graphs to Proof Nets: Boxes and Sharing in the
Graphical Presentation of Deductions, R. Kralovic and P. Urzyczyn
(Eds): Proceedings of MFCS 2006, LNCS Vol. 4162, Springer 2006,
pp. 3957. NB This pdf file is slightly different from the one
in the proceedings; a small mistake has been improved.
 L. Mamane, H. Geuvers
A DocumentOriented Coq Plugin for TEXmacs, paper presented at the
Mathematical UserInterfaces Workshop 2006 (as part of the Fifth
Mathematical Knowledge Management Conference) St Anne's Manor,
Workingham, United Kingdom, 2006 Aug 10th.
2004
 G. I. Jojgov and H. Geuvers,
A Calculus of Tactics and Its Operational Semantics, Proceedings of
the Mathematical Knowledge Management Symposium, Edinburgh 2003, ENTCS 93, Pages
118137, February 2004.
In case you are interested in "open terms and open proofs", see also the PhD thesis of Georgi Jojgov, Incomplete proofs and terms and their use in interactive theorem proving (PhD thesis, Eindhoven 2004).
 L. CruzFilipe, H. Geuvers, F. Wiedijk,
CCoRN,
the Constructive Coq Repository at Nijmegen In: Andrea Asperti,
Grzegorz Bancerek, Andrzej Trybulec (eds.), Mathematical Knowledge
Management, Proceedings of MKM 2004, Springer LNCS 3119, 88103, 2004.
 H. Geuvers, R. Nederpelt
Rewriting for Fitch style natural deductions
Proceedings of RTA 2004 (15th Internat. Conference on Rewriting Techniques and Applications, Aachen, Germany), ed. Vincent van Oostrom,
LNCS 3091, pp. 134154, Springer, 2004
 H. Geuvers, F. Wiedijk
A logical framework with explicit conversions. In: Carsten
Schürmann (ed.), LFM'04, Proceedings of the Fourth International
Workshop on Logical Frameworks and MetaLanguages, Cork, Ireland,
3245, 2004.
2003
 H. Geuvers and F. Wiedijk, editors,
Types for Proofs
and Programs: International Workshop Types 2002 [follow the workshop link to find some videos of the presentations], Berg en Dal, The
Netherlands, April 2002, selected papers, Springer LNCS 2646,
viii+331 pp. 2003.
 H. Geuvers and F. Kamareddine, editors,
Mathematics, Logic
and Computation, MLC 2003 , ICALP2003 workshop in honour of N.G. de
Bruijn's 85th anniversary, Electronic Notes in Theoretical Computer
Science 85 (7), Elsevier, 2003.
2002
 H. Geuvers and G. Jojgov,
Open terms and open proofs: a basis for interactive logic,
Computer Science Logic, CSL'02, Edinburgh, UK, Springer LNCS
2471, pp. 537552, 2002.
 H. Geuvers, R. Pollack, F. Wiedijk and J. Zwanenburg, A constructive
algebraic hierarchy in Coq, Journal of Symbolic Computation 34 (4),
pp. 271286, Elsevier, 2002.
Special Issue on the Integration of Automated Reasoning and
Computer Algebra Systems,
eds. S. Linton and R. Sebastiani,

H. Geuvers, M. Niqui,
Constructive Reals in Coq: Axioms and Categoricity , In
P. Callaghan, Z. Luo, J. McKinna, R. Pollack (Eds.), Proceedings of
TYPES 2000 Workshop, Durham, UK, LNCS 2277, SpringerVerlag, 2002,
pp. 7895.

H. Geuvers, F. Wiedijk, J. Zwanenburg,
A
Constructive Proof of the Fundamental Theorem of Algebra without Using
the Rationals. In P. Callaghan, Z. Luo, J. McKinna, R. Pollack
(Eds.), Proceedings of TYPES 2000 Workshop, Durham, UK, LNCS 2277,
SpringerVerlag, 2002, pp 96111.
2001
 M. Oostdijk and H. Geuvers,
Proof by Computation in the Coq
system, Theoretical Computer Science 272 (12), pp. 293  314, 2001.
 H. Geuvers, F. Wiedijk, J. Zwanenburg,
Equational Reasoning via Partial
Reflection©
SpringerVerlag ,
in Theorem Proving for Higher Order Logics, TPHOL 2000, Portland OR, USA,
eds. M. Aagaard and J. Harrison, LNCS 1869, pp. 162  178
 H. Barendregt and H. Geuvers,
Proof Assistants using Dependent
Type Systems, Chapter 18 of the Handbook of Automated
Reasoning (Vol 2), eds. A. Robinson and A. Voronkov, Elsevier 2001,
pp. 1149  1238.
 P.A.M. Seuren, V. Capretta and H. Geuvers,
The
logic and mathematics of occasion sentences,
Journal of Linguistics and Philosophy, 24, 2001, pp. 531595.
 H. Geuvers, R.Pollack, F. Wiedijk, J. Zwanenburg,
Skeleton for the Proof development leading
to the Fundamental Theorem of Algebra , Outline of the mathematics
of a constructive proof of the Fundamental Theorem of Algebra, which
we are formalising in Coq.
 H. Geuvers,
Induction is not derivable in second order
dependent type theory,©
SpringerVerlag ,
Proceedings of Typed
Lambda Calculus and Applications (TLCA 2001), Krakow, Poland, May
2001, ed. S. Abramsky, LNCS 2044, pp. 166181.
 H. Geuvers,
Inconsistency of classical logic in type
theory, Short Note (Version of November 27, 2001)

H. Geuvers , F. Wiedijk , J. Zwanenburg , R. Pollack , H.
Barendregt, (2001) A formalized proof of the Fundamental Theorem of
Algebra in the theorem prover Coq, Contributions to Coq V.7, April
2001, http://coq.inria.fr/contribs/fta.html (INRIARocquencourt).
Also available from the Helm Coqonline library (University of
Bologna): http://www.cs.unibo.it/helm/library.html
 O. Caprotti, H. Geuvers, and M. Oostdijk. Certified and Portable
Mathematical Documents from Formal Contexts, Electronic
Proceedings, of the 1st International Workshop on Mathematical
Knowledge Management, MKM2001, RISC, Schloss Hagenberg, Austria,
eds. B. Buchberger and O. Caprotti, 2001.
1999
 R. Bloo and H. Geuvers,
Explicit Substitution.
On the Edge of Strong Normalization, Theoretical Computer
Science 211 (1999), pp 375  395.
 H. Geuvers, E. Poll, J. Zwanenburg,
Safe
Proof Checking in Type Theory with Y ©
SpringerVerlag ,
in Proceedings of Computer
Science Logic 99 (8th Ann. Conf. of the EACSL), Madrid, Spain, eds. J.
Flum, M. RodriguezArtalejo, LNCS 1683, pp. 439  452
 H. Geuvers, E. Barendsen,
Some logical and syntactical
observations concerning the first
order dependent type system lambda P, MSCS vol. 94, 1999, pp. 335
 360
1997
 H. Geuvers,
Extending Models of Second
Order Predicate Logic to Models of Second Order Dependent Type Theory,
in Computer Science Logic, Annual Conference of the EACSL, Utrecht, September
1996, eds. D. van Dalen and M. Bezem, LNCS 1258, 1997, pp 167181.
 H. Geuvers,
Bunder, M., Dekkers, W., Geuvers, J.H.
Equivalence between illative combinatorry logics and pure type
systems. In T. Shimura (Ed.), Sequent calculus and Kripke semantics
for nonclassical logics, (RIMS Kokyuroku, 1021, pp. 119135). Kyoto:
RIMS.
1996
 G. Barthe and J.H. Geuvers,
Modular Properties of Algebraic Type Systems,
in Higherorder algebra, Logic and Term Rewriting, Paderborn, Germany,
1995, eds. G. Dowek, J. Heering, K. Meinke, B. M"oller, Springer,
LNCS 1074, Springer, 1996, pp. 3756.
 G. Barthe and J.H. Geuvers,
Congruence Types, in Computer Science Logic'95
, Paderborn, Germany, 1995, ed. H. Kleine B"uhning, LNCS 1092, Springer,
1996, pp. 3651.
 M. Stefanova and J.H. Geuvers,
A Simple Model Construction for the Calculus
of Constructions in Types for Proofs and Programs, Int. Workshop TYPES
'95, Torino, Italy, eds. S. Berardi and M. Coppo, Springer, LNCS 1158,
1996, pp. 249264.
1995
 J.H. Geuvers,
The Calculus of Constructions and Higher Order Logic, in The CurryHoward
isomorphism, ed. Ph. de Groote, Volume 8 of the "Cahiers du Centre
de logique" (Universit'e catholique de Louvain), Academia, LouvainlaNeuve
(Belgium), pp. 139191, 1995. (Preliminary version: The
Calculus of Constructions and Higher Order Logic)
 H. Geuvers,
A short and flexible proof of Strong Normalization
for the Calculus of Constructions in Types for Proofs and Programs,
Int. Workshop TYPES '94, Bastad, Sweden, Selected Papers, eds. P. Dybjer, B. Nordstr"om
and J. Smith, LNCS 996, pp 1438, Springer, 1995.
1994
 J.H. Geuvers and R.P. Nederpelt,
Untyped lambdacalculus, Typed lambdacalculus, sections 32 and 33 in Logic:
Mathematics, Language, Computer Science and Philosophy, Volume II, H.C.M.
de Swart et al., Peter Lang, Frankfurt am Main, 1994, pp 132199.
 J.H. Geuvers, Inductive and Coinductive
Types with Iteration and Recursion , in the informal proceedings of
the 1992 workshop on Types for Proofs and Programs, Bastad 1992, Sweden,
eds. B. Nordstrom, K. Petersson and G. Plotkin, pp 183207. In pdf
 J.H. Geuvers,
Conservativity between logics and typed lambdacalculi, in Types for Proofs
and Programs, Int. Workshop TYPES '93, Nijmegen, the Netherlands, eds.
H. Barendregt and T. Nipkow, Springer, LNCS 806, pp 79107, Springer 1994.
 J.H. Geuvers and B. Werner,
On the ChurchRosser property for Expressive
Type Systems and its Consequences for their Metatheoretic Study, in
Proceedings of the Ninth Annual Symposium on Logic in Computer Science,
Paris, France, IEEE Computer Society, pp 320329.
 F. Barbanera, M. Fernandez and H. Geuvers,
Modularity
of Strong Normalization in the lambdaalgebraiccube, in
Proceedings of the Ninth Annual Symposium on Logic in Computer
Science, Paris, France, IEEE Computer Society, pp
406415. (In pdf.)
 R.P. Nederpelt, J.H. Geuvers and R.C. de Vrijer (editors),
Selected Papers on Automath, Volume 133 in Studies in Logic and the Foundations
of Mathematics, NorthHolland, Amsterdam, 1994, pp 1024.
1993
 J.H. Geuvers (ed.),
Informal
Proceedings of the 1993 Workshop on Types for Proofs and Programs,
Nijmegen May 1993 (387 pp., ps file) To see the contents, see the Table
of Contents, ps file. Of some of the papers in these informal
proceedings, a final version has appeared in Types for Proofs and
Programs, Proc. of the Int. Workshop TYPES '93, Nijmegen, the
Netherlands, eds. H. Barendregt and T. Nipkow, Springer, LNCS 806,
Springer
 J.H. Geuvers,
Logics and Type systems, PhD. Thesis,
University of Nijmegen, September 1993.
1992
1991
 H. Geuvers, and M.J. Nederhof,
A modular proof of Strong Normalization for the Calculus of Constructions,
Journal of Functional Programming 1, 2 (1991), 155189.