Monotone Fixed-Point Types and Strong Normalization. - Ralph Matthes (CSL, 1998)

Monotone (co)inductive types and positive fixed-point types. - Ralph Matthes (RAIRO Theor. Informatics Appl., 1999)

Extensions of system F by iteration and primitive recursion on monotone inductive types. - Ralph Matthes (Utz, 1999)

Characterizing Strongly Normalizing Terms of a Calculus with Generalized Applications via Intersection Types. - Ralph Matthes (ICALP Satellite Workshops, 2000)

Standardization and Confluence for a Lambda Calculus with Generalized Applications. - Felix Joachimski; Ralph Matthes (RTA, 2000)

Monotone Inductive and Coinductive Constructors of Rank 2. - Ralph Matthes (CSL, 2001)

Interpolation for Natural Deduction with Generalized Eliminations. - Ralph Matthes (Proof Theory in Computer Science, 2001)

Parigot's Second Order lambda-mu-Calculus and Inductive Types. - Ralph Matthes (TLCA, 2001)

(Co-)Iteration for Higher-Order Nested Datatypes. - Andreas Abel 001; Ralph Matthes (TYPES, 2002)

Tarski's Fixed-Point Theorem And Lambda Calculi With Monotone Inductive Types. - Ralph Matthes (Synth., 2002)

Primitive Recursion for Rank-2 Inductive Types. - Andreas Abel 001; Ralph Matthes (FICS, 2003)

Generalized Iteration and Coiteration for Higher-Order Nested Datatypes. - Andreas Abel 001; Ralph Matthes; Tarmo Uustalu (FoSSaCS, 2003)

Short proofs of normalization for the simply- typed lambda-calculus, permutative conversions and Go"del's T. - Felix Joachimski; Ralph Matthes (Arch. Math. Log., 2003)

Fixed Points of Type Constructors and Primitive Recursion. - Andreas Abel 001; Ralph Matthes (CSL, 2004)

Substitution in non-wellfounded syntax with variable binding. - Ralph Matthes; Tarmo Uustalu (Theor. Comput. Sci., 2004)

Non-strictly positive fixed points for classical natural deduction. - Ralph Matthes (Ann. Pure Appl. Log., 2005)

Iteration and coiteration schemes for higher-order and nested datatypes. - Andreas Abel 001; Ralph Matthes; Tarmo Uustalu (Theor. Comput. Sci., 2005)

A Datastructure for Iterated Powers. - Ralph Matthes (MPC, 2006)

Verification of Programs on Truly Nested Datatypes in Intensional Type Theory. - Ralph Matthes (MSFP@MPC, 2006)

Verification of the Redecoration Algorithm for Triangular Matrices. - Ralph Matthes; Martin Strecker (TYPES, 2007)

Recursion on Nested Datatypes in Dependent Type Theory. - Ralph Matthes (CiE, 2008)

Nested Datatypes with Generalized Mendler Iteration: Map Fusion and the Example of the Representation of Untyped Lambda Calculus with Explicit Flattening. - Ralph Matthes (MPC, 2008)

Monadic Translation of Intuitionistic Sequent Calculus. - José Espírito Santo; Ralph Matthes; Luís Pinto 001 (TYPES, 2008)

Preface to the special issue: isomorphisms of types and invertibility of lambda terms. - Ralph Matthes; Sergei Soloviev 001 (Math. Struct. Comput. Sci., 2008)

Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi - José Espírito Santo; Ralph Matthes; Luís Pinto 001 (Log. Methods Comput. Sci., 2009)

An induction principle for nested datatypes in intensional type theory. - Ralph Matthes (J. Funct. Program., 2009)

Verification of the Schorr-Waite Algorithm - From Trees to Graphs. - Mathieu Giorgino; Martin Strecker; Ralph Matthes; Marc Pantel (LOPSTR, 2010)

Verification of redecoration for infinite triangular matrices using coinduction. - Ralph Matthes; Célia Picard (TYPES, 2011)

Coinductive Graph Representation: the Problem of Embedded Lists. - Célia Picard; Ralph Matthes (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011)

Map fusion for nested datatypes in intensional type theory. - Ralph Matthes (Sci. Comput. Program., 2011)

Permutations in Coinductive Graph Representation. - Célia Picard; Ralph Matthes (CMCS, 2012)

Preface to the special issue: commutativity of algebraic diagrams. - Ralph Matthes; Sergei Soloviev 001 (Math. Struct. Comput. Sci., 2012)

On a Dynamic Logic for Graph Rewriting. - Mathias Winckel; Ralph Matthes (ICTERI, 2013)

A Coinductive Approach to Proof Search. - José Espírito Santo; Ralph Matthes; Luís Pinto 001 (FICS, 2013)

Preface. - Ralph Matthes; Tarmo Uustalu (RAIRO Theor. Informatics Appl., 2013)

Monadic translation of classical sequent calculus. - José Espírito Santo; Ralph Matthes; Koji Nakazawa; Luís Pinto 001 (Math. Struct. Comput. Sci., 2013)

Confluence for classical logic through the distinction between values and computations. - José Espírito Santo; Ralph Matthes; Koji Nakazawa; Luís Pinto 001 (CL&C, 2014)

Heterogeneous Substitution Systems Revisited. - Benedikt Ahrens; Ralph Matthes (TYPES, 2015)

Preface. - David Baelde; Arnaud Carayol; Ralph Matthes; Igor Walukiewicz (Fundam. Informaticae, 2017)

Martin Hofmann's Case for Non-Strictly Positive Data Types. - Ulrich Berger 001; Ralph Matthes; Anton Setzer (TYPES, 2018)

Certification of Breadth-First Algorithms by Extraction. - Dominique Larchey-Wendling; Ralph Matthes (MPC, 2019)

Decidability of Several Concepts of Finiteness for Simple Types. - José Espírito Santo; Ralph Matthes; Luís Pinto 001 (Fundam. Informaticae, 2019)

From Signatures to Monads in UniMath. - Benedikt Ahrens; Ralph Matthes; Anders Mörtberg (J. Autom. Reason., 2019)

Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search. - José Espírito Santo; Ralph Matthes; Luís Pinto 001 (Math. Struct. Comput. Sci., 2019)

Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic. - José Espírito Santo; Ralph Matthes; Luís Pinto 001 (TYPES, 2020)

Proof search for full intuitionistic propositional logic through a coinductive approach for polarized logic. - José Espírito Santo; Ralph Matthes; Luís Pinto 001 (CoRR, 2020)

A coinductive approach to proof search through typed lambda-calculi. - José Espírito Santo; Ralph Matthes; Luís Pinto 001 (Ann. Pure Appl. Log., 2021)

Implementing a category-theoretic framework for typed abstract syntax. - Benedikt Ahrens; Ralph Matthes; Anders Mörtberg (CPP, 2022)

Univalent Monoidal Categories. - Kobe Wullaert; Ralph Matthes; Benedikt Ahrens (TYPES, 2022)

Formalizing Monoidal Categories and Actions for Syntax with Binders. - Benedikt Ahrens; Ralph Matthes; Kobe Wullaert (CoRR, 2023)

Substitution for Non-Wellfounded Syntax with Binders. - Ralph Matthes; Kobe Wullaert; Benedikt Ahrens (CoRR, 2023)

Displayed Monoidal Categories for the Semantics of Linear Logic. - Benedikt Ahrens; Ralph Matthes; Niels van der Weide; Kobe Wullaert (CPP, 2024)

Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories. - Ralph Matthes; Kobe Wullaert; Benedikt Ahrens (FSCD, 2024)