| 2024 | CPP | Displayed Monoidal Categories for the Semantics of Linear Logic. | Benedikt Ahrens, Ralph Matthes, Niels van der Weide, Kobe Wullaert |
| 2024 | FSCD | Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories. | Ralph Matthes, Kobe Wullaert, Benedikt Ahrens |
| 2022 | CPP | Implementing a category-theoretic framework for typed abstract syntax. | Benedikt Ahrens, Ralph Matthes, Anders Mrtberg |
| 2019 | MPC | Certification of Breadth-First Algorithms by Extraction. | Dominique Larchey-Wendling, Ralph Matthes |
| 2013 | ICTERI | On a Dynamic Logic for Graph Rewriting. | Mathias Winckel, Ralph Matthes |
| 2010 | LOPSTR | Verification of the Schorr-Waite Algorithm - From Trees to Graphs. | Mathieu Giorgino, Martin Strecker, Ralph Matthes, Marc Pantel |
| 2008 | CiE | Recursion on Nested Datatypes in Dependent Type Theory. | Ralph Matthes |
| 2008 | MPC | Nested Datatypes with Generalized Mendler Iteration: Map Fusion and the Example of the Representation of Untyped Lambda Calculus with Explicit Flattening. | Ralph Matthes |
| 2006 | MPC | A Datastructure for Iterated Powers. | Ralph Matthes |
| 2006 | MPC | Verification of Programs on Truly Nested Datatypes in Intensional Type Theory. | Ralph Matthes |
| 2004 | CSL | Fixed Points of Type Constructors and Primitive Recursion. | Andreas Abel, Ralph Matthes |
| 2003 | FOSSACS | Generalized Iteration and Coiteration for Higher-Order Nested Datatypes. | Andreas Abel, Ralph Matthes, Tarmo Uustalu |
| 2001 | CSL | Monotone Inductive and Coinductive Constructors of Rank 2. | Ralph Matthes |
| 2000 | ICALP | Characterizing Strongly Normalizing Terms of a Calculus with Generalized Applications via Intersection Types. | Ralph Matthes |
| 1998 | CSL | Monotone Fixed-Point Types and Strong Normalization. | Ralph Matthes |