- (CSL 98) A manuscript on "Monotone Fixed-Point Types And Strong Normalization" (15 pages, August 1998; original submission 12 pages, April 1998, © Springer Verlag)
- (Archive for Mathematical Logic 42 (2003) 1, 59-87) A manuscript on "Short Proofs of Normalization" (latest version 23 pages, April 2002). Math. Reviews 1953114. Erratum to all versions since 1999 (2 pages, November 2004)
- (FICS 98, RAIRO - Theoretical Informatics and Applications 33, pp. 309-328, 1999) A manuscript on "Monotone (co)inductive types and positive fixed-point types" (20 pages, June 1999; original submission 20 pages, November 1998)
- (FotFS I, Synthese 133(1), pp. 107-129, October 2002) A manuscript on "Tarski's fixed-point theorem and higher-order term rewrite systems" (25 pages, December 1999; older version 21 pages, August 1999). Math. Reviews 1950046
- (ITRS 00) A manuscript on "Characterizing Strongly Normalizing Terms for a Lambda Calculus with Generalized Applications via Intersection Types" (15 pages, April 2000; original submission 15 pages, March 2000)
- (RTA 00) A manuscript on "Standardization and Confluence for a Lambda Calculus with Generalized Applications" (15 pages, March 2000, © Springer Verlag)
- (TLCA 01) A manuscript on "Parigot's Second Order Lambda-Mu-Calculus and Inductive Types" (15 pages, February 2001; original submission 15 pages, October 2000; © Springer Verlag)
- (CSL 01) A manuscript on "Monotone Inductive and Coinductive Constructors of Rank 2" (15 pages, June 2001; original submission 16 pages, March 2001; © Springer Verlag)
- (PTCS, appeared 2001) A manuscript on "Interpolation for natural deduction with generalized eliminations" (17 pages, July 2001; © Springer Verlag). Math. Reviews 1904416 (2003h:03023)
- (FOSSACS 2003) A manuscript on "Generalized Iteration and Coiteration for Higher-Order Nested Datatypes" (15 pages, January 2003; © Springer Verlag)
- (TYPES 2002) A manuscript on "(Co-)Iteration for Higher-Order Nested Datatypes" (20 pages, February 2003; © Springer Verlag)
- (CMCS 03, ENTCS Vol.82.1) A manuscript on "Substitution in Non-wellfounded Syntax with Variable Binding" (15 pages, February 2003). A preliminary version (24 pages, April 2004) of the full paper in TCS 327 (1-2) pp. 155-174, 2004
- (APAL 133, pp. 205-230, 2005) A manuscript on "Non-Strictly Positive Fixed-Points for Classical Natural Deduction" (33 pages, September 2003, Erratum: there is no distinction between admissible and derived rules; original submission 31 pages, July 2003, errata for the older version)
- (Proceedings of Logic Colloquium 2003, pp. 167-199, Lecture Notes in Logic Vol. 24, © Association for Symbolic Logic) A manuscript on "Stabilization - An Alternative to Double-Negation Translation for Classical Natural Deduction" (25 pages, January 2004, this is only the original submission, as PDF; later changes). Note that the printed version has three lines that begin with a multiplication sign as if the terms in parentheses were multiplied (pp. 174, 181, 191). This was not intended.
- (CSL 04) A manuscript on "Fixed Points of Type Constructors and Primitive Recursion" (15 pages, June 2004; as PDF; Erratum, October 2004; original submission 16 pages, April 2004; © Springer Verlag)
- (TCS 333(1-2), pp. 3-66, 2005) A manuscript on "Iteration and Coiteration Schemes for Higher-Order and Nested Datatypes (79 pages, March 2004; Erratum, August 2005; original submission 58 pages, August 2003)

- (MPC 06) A manuscript on "A Datastructure for Iterated Powers" (16 pages, April 2006; © Springer Verlag: MPC '06 Proceedings, LNCS 4014, pp. 299-315). Implementation of n Times Nested Bushes in Coq.
- (MSFP 06) A manuscript on "Verification of programs on truly nested datatypes in intensional type theory" (12 pages, June 2006; published in eWiC series, free access to the published article). Implementation in Coq. The paper and the implementation are superseded by the journal version for JFP, see below.
- (TLCA 07) A manuscript on "Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi" (15 pages, April 2007; © Springer Verlag: TLCA 2007 Proceedings, LNCS 4583, pp. 133-147). There is also a journal version for LMCS, see below.
- (TYPES 2007) A manuscript on "Verification of the Redecoration Algorithm for Triangular Matrices" (17 pages, December 2007, © Springer Verlag: TYPES 07 Post-Proceedings, LNCS 4941, pp. 125-141). Coq and Isabelle scripts for the article.
- (JFP 19(3&4) pp.439-468, 2009) The paper "An induction principle for nested datatypes in intensional type theory" (30 pages, June 2009, © Cambridge University Press, online in the Journal of Functional Programming). Implementation in Coq.
- (CiE 08) A manuscript on "Recursion on Nested Datatypes in Dependent Type Theory" (16 pages, March 2008; © Springer Verlag: CiE 08 Proceedings, LNCS 5028, pp. 431-446). Implementation in Coq.
- (MPC 08) A manuscript on "Nested datatypes with generalized Mendler iteration: map fusion and the example of the representation of untyped lambda calculus with explicit flattening" (23 pages, April 2008; © Springer Verlag: MPC 08 Proceedings, LNCS 5133, pp. 220-242). Implementation in Coq. There is also a journal version for SCP, see below.
- (LMCS 2009 (5) 2:11) "Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi" (36 pages, May 2009; published in Logical Methods in Computer Science). A local copy of the PDF file.
- (TYPES 2008) A manuscript on "Monadic translation of intuitionistic sequent calculus" (17 pages, February 2009; © Springer Verlag: TYPES '08 Proceedings, LNCS 5497, pp. 100-116).
- (SCP 76(3), pp.204-224, 2011) A manuscript on "Map Fusion for Nested Datatypes in Intensional Type Theory" (33 pages, February 2010; © Elsevier: online version). Implementation in Coq.
- (LOPSTR 2010) A manuscript on "Verification of the Schorr-Waite algorithm - From trees to graphs" (16 pages, January 2011; © Springer Verlag: Post-Proceedings 2011, LNCS 6564, pp. 67-83 ). Implementation in Isabelle.
- (ECEASST, vol. 39, 2011) The paper "Coinductive Graph Representation: the Problem of Embedded Lists" (24 pages, September 2011) in the open access journal Electronic Communications of the EASST (ISSN 1863-2122), volume 39, the post-proceedings of the Graph Computation Models 2010 with selected revised papers.
- (CMCS 2012) A manuscript on "Permutations in Coinductive Graph Representation" (20 pages, February 2012, © Springer Verlag: Coalgebraic Methods in Computer Science 2012, Revised Selected Papers, LNCS 7399, pp. 218-237, presented at CMCS 2012 in Tallinn). Implementation in Coq. A more complete treatment is found in Celia Picard's thesis.
- (MSCS 23(6), pp.1111 - 1162, 2013) The paper "Monadic translation of classical sequent calculus" by José Espírito Santo, Ralph Matthes, Koji Nakazawa and Luís Pinto (52 pages, published online in January 2013 in Mathematical Structures in Computer Science, © Cambridge University Press).
- (TYPES 2011, LIPIcs, vol.19, pp.55-69) The paper "Verification of redecoration for infinite triangular matrices using coinduction" (15 pages, January 2013, published in LIPIcs in the post-proceedings of TYPES 2011). Implementation in Coq.
- (SMSV 2013) A manuscript on "On a Dynamic Logic for Graph Rewriting" (15 pages, June 2013, Vol. 1000 of CEUR Workshop Proceedings).
- (FICS 2013) The paper "A Coinductive Approach to Proof Search" (16 pages, published in August 2013 by EPTCS, volume 126, pages 28-43, DOI: 10.4204/EPTCS.126.3 for the paper and 10.4204/EPTCS.126 for the volume).
- (CL&C 2014) A paper on "Confluence for classical logic through the distinction between values and computations" (15 pages, published in September 2014 by EPTCS, volume 164, pages 63-77, DOI: 10.4204/EPTCS.164.5 for the paper and 10.4204/EPTCS.164 for the volume).
- (TYPES 2015 - LIPIcs volume 69 of 2018) "Heterogeneous substitution systems revisited" (23 pages, local copy). A draft version is available on arXiv as "Heterogeneous substitution systems revisited" (24 pages, January 2016, local copy).
- (MSCS 29, pp.1092-1124, 2019) The paper "Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search" (31 pages before typesetting by CUP, February 2018). Draft version at arXiv (19 pages, March 2017, local copy). DOI: 10.1017/S0960129518000099, Mathematical Structures in Computer Science, © Cambridge University Press.
- (JAR 63(2), pp.285-318, 2019) The paper "From signatures to monads in UniMath" (34 pages, June 2018, local copy). A draft version is available on arXiv as "From signatures to monads in UniMath" (30 pages, December 2016, local copy).
- (Fundamenta Informaticae 170(1-3), pp.111-138, 2019) The paper "Decidability of Several Concepts of Finiteness for Simple Types" (published October 2019, preprint available on HAL).
- (MPC 2019, LNCS 11825, pp.45-75, 2019) The paper "Certification of Breadth-First Algorithms by Extraction" © Springer Nature Switzerland (published October 2019, will become available on HAL, pre-print version).
- (TYPES 2018 - LIPIcs volume 130 of 2019) The paper "Martin Hofmannâ€™s Case for Non-Strictly Positive Data Types" (22 pages, November 2019).
- (TYPES 2020 - LIPIcs volume 188 of 2021) The paper "Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic" (24 pages, June 2021).
- (APAL, in press) The paper "A coinductive approach to proof search through typed lambda-calculi" © Elsevier B.V. (45 pages, available online since July 27, 2021), a preliminary version under the same title is available at arXiv (39 pages, August 2020).

- (unpublished) Lecture notes on "Lambda Calculus: A Case for Inductive Definitions" for ESSLLI 2000 (65 pages, July 2000; as Postscript, PS Version at half size), Errata, Part II: Monotone Inductive Types (20 pages, August 2000, as Postscript)

Ask DBLP (does not show FotFS I in Synthese and Logic Colloquium 2003) and Citeseer.

For my publications considered to fall also within mathematics, ask MathSciNet (needs a subscription). The citation counts shown there are those from other papers considered to fall within mathematics.

My coauthors:

- Andreas Abel: TYPES 2002, FOSSACS 2003, CSL 2004, TCS
- Benedikt Ahrens: TYPES 2015, JAR
- Ulrich Berger: TYPES 2018
- José Espírito Santo: TLCA 2007, LMCS, TYPES 2008, 2x MSCS, FICS 2013, CL&C 2014, FI, TYPES 2020, APAL
- Mathieu Giorgino: LOPSTR 2010
- Felix Joachimski: RTA 2000, Archive for Mathematical Logic
- Dominique Larchey-Wendling: MPC 2019
- Anders MĂ¶rtberg: JAR
- Koji Nakazawa: MSCS, CL&C 2014
- Celia Picard: ECEASST, CMCS 2012, TYPES 2011
- Marc Pantel: LOPSTR 2010
- Luís Pinto: TLCA 2007, LMCS, TYPES 2008, 2x MSCS, FICS 2013, CL&C 2014, FI, TYPES 2020, APAL
- Anton Setzer: TYPES 2018
- Martin Strecker: TYPES 2007, LOPSTR 2010
- Tarmo Uustalu: FOSSACS 2003, CMCS 2003, 2x TCS
- Mathias Winckel: SMSV 2013

Ralph Matthes Last modified (date in French): Wed Jul 28 15:12:11 CEST 2021