Publications of Herman Geuvers

See my dblp entry.

2022

• Herman Geuvers, Rob Nederpelt
  Characteristics of de Bruijn's early proof checker Automath. Fundam. Informaticae 185(4), pp. 313-336 (2022)
• Herman Geuvers
  Apartness and Distinguishing Formulas in Hennessy-Milner Logic. A Journey from Process Algebra via Timed Automata to Model Learning 2022 (Essays Dedicated to Frits W. Vaandrager on the Occasion of His 60th Birthday, LNCS 13560, Springer), pp. 266-282
• Ike Mulder, Robbert Krebbers, Herman Geuvers
  Diaframe: automated verification of fine-grained concurrent programs in Iris. PLDI 2022, pp. 809-824
• Herman Geuvers, Anton Golov
  Directed branching bisimulation via apartness and positive logic. CoRR abs/2210.07380

2021

• Herman Geuvers, Bart Jacobs
  Relating Apartness and Bisimulation. Log. Methods Comput. Sci. 17(3) (2021)

2020

• Lasse Blaauwbroek, Josef Urban, Herman Geuvers
  Tactic Learning and Proving for the Coq Proof Assistant, LPAR23, 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (editors Elvira Albert and Laura Kovacs), EPiC Series in Computing Volume 73, 2020, pp 138-150, 2020.
• Lasse Blaauwbroek, Josef Urban, Herman Geuvers
  The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq, In: Benzmuller C., Miller B. (eds) Intelligent Computer Mathematics. CICM 2020. Lecture Notes in Computer Science, vol 12236. Springer, pp. 271-277.
• Herman Geuvers, Bart Jacobs
  Relating Apartness and Bisimulation, on arXiv (2020)
• Lasse Blaauwbroek, Josef Urban, Herman Geuvers
  The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq, on arXiv (2020).

2019

• Herman Geuvers, Iris van der Giessen and Tonny Hurkens
  Strong Normalization for Truth Table Natural Deduction, Fundamenta Informaticae, vol. 170, no. 1-3, pp. 139-176, 2019.
  Also see the Master thesis Mathematics of Iris van der Giessen, Natural Deduction Derived from Truth Tables of July 2018.
• Niels van der Weide and Herman Geuvers
  The Construction of Set-Truncated Higher Inductive Types, proceedings of MFPSXXXV, London, UK, Elsevier Electronic Notes in Theoretical Computer Science Volume 347, 2019, Pages 261-280.
• Herman Geuvers (editor)
  4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), FSCD 2019, June 24-30, 2019, Dortmund, Germany, Leibniz International Proceedings in Informatics (LIPIcs) vol. 131, 2019, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.

2018

• Herman Geuvers and Tonny Hurkens
  Proof Terms for Generalized Natural Deduction, In 23rd International Conference on Types for Proofs and Programs (TYPES 2017), editors A. Abel, F. Nordvall Forsberg and A. Kaposi, LIPIcs Vol 104, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2018, pages 3:1--3:39.
  • Herman Geuvers and Tonny Hurkens -- Addendum to Proof Terms for Generalized Natural Deduction (to provide some additional details for the strong normalization proof and to repair a few omissions in the definitions.)
• Dan Frumin, Herman Geuvers, Leon Gondelman, Niels van der Weide
  Finite sets in homotopy type theory, CPP, pp. 201--214, ACM 2018.
• Silvia Ghilezan and Herman Geuvers and Jelena Ivetic (Eds.)
  Proceedings of the 22nd International Conference on Types for Proofs and Programs, Types 2016. Post-conference proceedings of TYPES 2016, May 23-26, 2016 - Novi Sad, Serbia. ISBN 978-3-95977-065-1, LIPICS Vol. 97.

2017

• Henning Basold, Herman Geuvers, Niels van der Weide
  Higher Inductive Types in Programming, Journal of Universal Computer Science, Vol. 23, No. 1, pp. 63-88.
• Herman Geuvers, Tonny Hurkens
  Deriving Natural Deduction Rules from Truth Tables. In S. Ghosh and S. Prasad, editors, Logic and Its Applications - 7th Indian Conference, ICLA 2017, Kanpur, India, January 5-7, 2017, Proceedings. Lecture Notes in Computer Science 10119, Springer, pp. 123-138. For a preliminary version, see here.
• Myrthe van Delft, Herman Geuvers, Tim Willemse
  A Formalisation of Consistent Consequence for Boolean Equation Systems. ITP 2017, Lecture Notes in Computer Science 10499, Springer, pp. 462--478.
• Herman Geuvers, Matthew England, Osman Hasan, Florian Rabe, Olaf Teschke, editors
  Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings, Lecture Notes in Computer Science 10383, Springer.

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. 177-183.
• 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 183--207.

2015

• Herman Geuvers
  The Church-Scott representation of inductive and coinductive data, manuscript.
• Herman Geuvers
  A typed lambda calculus with call-by-name and call-by-value iteration, manuscript.
• H. Geuvers and J. Verkoelen,
  The non-typability of some fixed-point combinators in Pure Type Systems, submitted.

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 meta-theory 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. 1-18.
• Cezary Kaliszyk, Josef Urban, Jiri Vyskocil, Herman Geuvers
  Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description. CICM 2014, LNCS 8543, Springer, pp. 435-439.

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 1034-1049, In memory of N.G. (Dick) de Bruijn (1918-2012), 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 24-25, 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 meta-languages: theory and practice, Boston USA, September 2013, ACM (digital library).
• H. Geuvers, R. Krebbers and J. McKinna,
  The lambda-mu-T-calculus. In volume 164, issue 6 of APAL, pages 676-701. [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: 71-83 (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. 795-803
• H. Geuvers, R. Krebbers,
  The correctness of Newman's typability algorithm and some of its extensions. Theor. Comput. Sci. 412(28): 3242-3261 (2011)
• J. Endrullis, H. Geuvers, J. G. Simonsen and H. Zantema,
  Levels of Undecidability in Rewriting. In: Information and Computation 209 (2). 2011. pp. 227-245.
• H. Geuvers, G. Nadathur (editors)
  Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: 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 22-25, 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. 298-300
• Daniel Kuehlwein, Josef Urban, Evgeni Tsivtsivadze, Herman Geuvers, Tom Heskes
  Multi-output Ranking for Automated Reasoning. KDIR 2011 - Proceedings of the International Conference on Knowledge Discovery and Information Retrieval, Paris, France, 26-29 October, 2011. SciTePress 2011, pp. 42-51

2010

• H. Geuvers, A. Koprowski, D. Synek and E. van der Weegen
  Automated Machine-Checked Hybrid System Safety Proofs. In LNCS 6172, eds. M. Kaufmann and L. Paulson, conference on Interactive Theorem Proving, Edinburgh UK, pp. 259-274, Springer.
• C. Tankink, H. Geuvers, J. McKinna and F. Wiedijk,
  Proviola: a Tool for Proof Re-animation, Conference on Intelligent Computer Mathematics (CICM), Paris. LNCS 6167,2010, pp. 440-454, 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. 455-469, 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 Meta-languages: Theory and Practice (LFMTP). EPTCS 34 2010, pages 53-67.

2009

• A. Asperti, H. Geuvers and N. Raja,
  Social processes, program verification and all that, Math. Struct. in Comp. Science, vol. 19, pp. 877-896, Cambridge University Press 2009.
• S. Barry Cooper, Herman Geuvers, Anand Pillay and Jouko A. Vaananen (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. 255-270, 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 3-25.
• L. Mamane, H. Geuvers, J. McKinna
  A Logically Saturated Extension of lambda-bar-mu-mu-tilde, in Proceedings of 8th International Conference MKM, Grand Bend, Canada, July 6-12, 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 lambda-bar-mu-mu-tilde. Technical Report, Radboud University Nijmegen. ICIS--R09002. 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 1-2, 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 Meta-Languages, Cork, Ireland, Electronic Notes in Theoretical Computer Science, Volume 199, 24 February 2008, Pages 33-47.
• 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 93-108.
• 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. Skaf-Molli, M. Völkel, CEUR Workshop Proceedings ISSN 1613-0073, 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 485-526, 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 3-36, 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 18-21, 2006, Revised Selected Papers. Edited by Thorsten Altenkirch and Conor McBride. LNCS 4502, 2007. pp. 140-159.
• H. Geuvers
  Computer-ondersteund redeneren: de boekhouder steunt de denker (Dutch)
  inaugural speech , Radboud University Nijmegen, March 9 2007, ISBN 978-90-9021687-4.
• H. Geuvers
  Computer-ondersteund 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. 315--329.
• 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. 39--57. NB This pdf file is slightly different from the one in the proceedings; a small mistake has been improved.
• L. Mamane, H. Geuvers
  A Document-Oriented Coq Plugin for TEXmacs, paper presented at the Mathematical User-Interfaces 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 118-137, 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. Cruz-Filipe, H. Geuvers, F. Wiedijk,
  C-CoRN, the Constructive Coq Repository at Nijmegen In: Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec (eds.), Mathematical Knowledge Management, Proceedings of MKM 2004, Springer LNCS 3119, 88-103, 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. 134-154, 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 Meta-Languages, Cork, Ireland, 32-45, 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 , ICALP-2003 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. 537--552, 2002.
• H. Geuvers, R. Pollack, F. Wiedijk and J. Zwanenburg, A constructive algebraic hierarchy in Coq, Journal of Symbolic Computation 34 (4), pp. 271--286, 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, Springer-Verlag, 2002, pp. 78-95.
• 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, Springer-Verlag, 2002, pp 96-111.

2001

• M. Oostdijk and H. Geuvers,
  Proof by Computation in the Coq system, Theoretical Computer Science 272 (1-2), pp. 293 -- 314, 2001.
• H. Geuvers, F. Wiedijk, J. Zwanenburg,
  Equational Reasoning via Partial Reflection© Springer-Verlag , 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. 531--595.
• 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,© Springer-Verlag , Proceedings of Typed Lambda Calculus and Applications (TLCA 2001), Krakow, Poland, May 2001, ed. S. Abramsky, LNCS 2044, pp. 166--181.
• 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 (INRIA-Rocquencourt). Also available from the Helm Coq-on-line 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 Know-ledge 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 © Springer-Verlag , in Proceedings of Computer Science Logic 99 (8th Ann. Conf. of the EACSL), Madrid, Spain, eds. J. Flum, M. Rodriguez-Artalejo, 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. 9-4, 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 167--181.
• 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 non-classical logics, (RIMS Kokyuroku, 1021, pp. 119-135). Kyoto: RIMS.

• G. Barthe and J.H. Geuvers,
  Modular Properties of Algebraic Type Systems, in Higher-order algebra, Logic and Term Rewriting, Paderborn, Germany, 1995, eds. G. Dowek, J. Heering, K. Meinke, B. M"oller, Springer, LNCS 1074, Springer, 1996, pp. 37--56.
• 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. 36--51.
• 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. 249--264.

1995

• J.H. Geuvers,
  The Calculus of Constructions and Higher Order Logic, in The Curry-Howard isomorphism, ed. Ph. de Groote, Volume 8 of the "Cahiers du Centre de logique" (Universit'e catholique de Louvain), Academia, Louvain-la-Neuve (Belgium), pp. 139-191, 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 14--38, Springer, 1995.

1994

• J.H. Geuvers and R.P. Nederpelt,
  Untyped lambda-calculus, Typed lambda-calculus, 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 132--199.
• 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 183--207. In pdf
• J.H. Geuvers,
  Conservativity between logics and typed lambda-calculi, in Types for Proofs and Programs, Int. Workshop TYPES '93, Nijmegen, the Netherlands, eds. H. Barendregt and T. Nipkow, Springer, LNCS 806, pp 79-107, Springer 1994.
• J.H. Geuvers and B. Werner,
  On the Church-Rosser 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 320--329.
• F. Barbanera, M. Fernandez and H. Geuvers,
  Modularity of Strong Normalization in the lambda-algebraic-cube, in Proceedings of the Ninth Annual Symposium on Logic in Computer Science, Paris, France, IEEE Computer Society, pp 406--415. (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, North-Holland, 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., pdf file) To see the contents, see the Table of Contents, pdf 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

• J.H. Geuvers,
  The Church-Rosser property for beta-eta-reduction in typed lambda calculi. In Proceedings of the seventh annual symposium on Logic in Computer Science, Santa Cruz, Cal., IEEE, pp 453-460, 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), 155--189.