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 2010) A manuscript on "Map Fusion for Nested Datatypes in Intensional Type Theory" (33 pages, February 2010; © Elsevier: online version). 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; Version in original size), Errata, Part II: Monotone Inductive Types (20 pages, August 2000)

Ask DBLP (does not show FotFS I, Logic Colloquium 2003, MSFP 06) and Citeseer.

My coauthors:

• Andreas Abel: TYPES 2002, FOSSACS 2003, CSL 2004, TCS
• José Carlos Espírito Santo: TLCA 2007, LMCS, TYPES 2008
• Felix Joachimski: RTA 2000, Archive for Mathematical Logic
• Luís Pinto: TLCA 2007, LMCS, TYPES 2008
• Martin Strecker: TYPES 2007
• Tarmo Uustalu: FOSSACS 2003, CMCS 2003, 2x TCS