Published and unpublished work by Ralph Matthes

Thesis

Preprints of Published Work

• (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 now 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 now 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 ).
• (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.
• (MSCS) 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.

Unpublished and Submitted Work

• (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, Logic Colloquium 2003, MSFP 06, MSCS, TYPES 2011) 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
• José Carlos Espírito Santo: TLCA 2007, LMCS, TYPES 2008, MSCS
• Mathieu Giorgino: LOPSTR 2010
• Felix Joachimski: RTA 2000, Archive for Mathematical Logic
• Koji Nakazawa: MSCS
• Celia Picard: ECEASST, CMCS 2012, TYPES 2011
• Marc Pantel: LOPSTR 2010
• Luís Pinto: TLCA 2007, LMCS, TYPES 2008, MSCS
• Martin Strecker: TYPES 2007, LOPSTR 2010
• Tarmo Uustalu: FOSSACS 2003, CMCS 2003, 2x TCS