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.)
Entry in the catalogue of the German National Library.
Review
in ZBL.
My
advisor has been Prof.
Dr. Helmut Schwichtenberg.
Preprints of Published Work
See also my ORCID (the publication list there is in particular lacking workshops, except for those that have proceedings in LNCS).
- (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 lambda calculi with monotone inductive types" (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 and until 2019,
consult
the IRIT database. The more recent papers are all found when searching for my family name at HAL interface of IRIT.
- (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, 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 172, Issue 10, December 2021, page numbers not yet public) 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).
- (CPP 2022) The paper "Implementing a Category-Theoretic Framework for Typed Abstract Syntax" (17 pages, January 2022), in Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '22), 2022, ACM, New York, NY, USA. A preliminary version under the same title is available at arXiv (17 pages, December 2021).
- (TYPES 2022 - LIPIcs volume 269 of 2023) The paper "Univalent Monoidal Categories" (21 pages, July 2023), in Postproceedings of 28th International Conference on Types for Proofs and Programs (TYPES 2022).
Unpublished and Submitted Work
Ask DBLP
(does not show Logic Colloquium 2003).
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 (for published papers):
- Andreas
Abel: TYPES 2002, FOSSACS 2003, CSL 2004, TCS
- Benedikt Ahrens: TYPES 2015, JAR, CPP 2022, TYPES 2022
- 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, CPP 2022
- 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
- Kobe Wullaert: TYPES 2022
Ralph Matthes
Last modified (date in French): lun. août 14 18:24:05 CEST 2023
https://www.irit.fr/~Ralph.Matthes/works.html