Published and unpublished work by Ralph Matthes
Thesis
The title of my doctoral dissertation is "Extensions of
System F by Iteration and Primitive Recursion on Monotone Inductive
Types". Available as PDF file (just the
introduction and summary), Postscript file, and DVI file and Postscript file with 2 pages
per sheet. (197 pages, June 1999, minor revision of the
submission of
May 1998. There are also Errata.) Review
in ZBL.
My
advisor has been Prof.
Dr. Helmut Schwichtenberg.
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)
For proper citations, BibTeX entries and abstracts of papers that
appeared since 2006,
consult
the IRIT database.
- (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
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
Ralph Matthes
Last modified: Wed Jun 23 17:04:49 CEST 2010
http://www.irit.fr/~Ralph.Matthes/works.html