Ralph Matthes

ORCID

Publication Activity (10 Years)

Years Active: 1998-2024
Publications (10 Years): 21

Top Venues

Ludwig Maximilian University of Munich, Germany (PHD)

Education History

Ludwig Maximilian University of Munich, Germany

PHD

Publications

Ralph Matthes, Kobe Wullaert, Benedikt Ahrens
Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories. FSCD (2024)
Benedikt Ahrens, Ralph Matthes, Niels van der Weide, Kobe Wullaert
Displayed Monoidal Categories for the Semantics of Linear Logic. CPP (2024)
Ralph Matthes, Kobe Wullaert, Benedikt Ahrens
Substitution for Non-Wellfounded Syntax with Binders. CoRR (2023)
Benedikt Ahrens, Ralph Matthes, Kobe Wullaert
Formalizing Monoidal Categories and Actions for Syntax with Binders. CoRR (2023)
Kobe Wullaert, Ralph Matthes, Benedikt Ahrens
Univalent Monoidal Categories. CoRR (2022)
Benedikt Ahrens, Ralph Matthes, Anders Mörtberg
Implementing a category-theoretic framework for typed abstract syntax. CPP (2022)
Kobe Wullaert, Ralph Matthes, Benedikt Ahrens
Univalent Monoidal Categories. TYPES (2022)
Benedikt Ahrens, Ralph Matthes, Anders Mörtberg
Implementing a Category-Theoretic Framework for Typed Abstract Syntax. CoRR (2021)
José Espírito Santo, Ralph Matthes, Luís Pinto
A coinductive approach to proof search through typed lambda-calculi. Ann. Pure Appl. Log. 172 (10) (2021)
José Espírito Santo, Ralph Matthes, Luís Pinto
Proof search for full intuitionistic propositional logic through a coinductive approach for polarized logic. CoRR (2020)
José Espírito Santo, Ralph Matthes, Luís Pinto
Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic. TYPES (2020)
José Espírito Santo, Ralph Matthes, Luís Pinto
Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search. Math. Struct. Comput. Sci. 29 (8) (2019)
Dominique Larchey-Wendling, Ralph Matthes
Certification of Breadth-First Algorithms by Extraction. MPC (2019)
Benedikt Ahrens, Ralph Matthes, Anders Mörtberg
From Signatures to Monads in UniMath. J. Autom. Reason. 63 (2) (2019)
José Espírito Santo, Ralph Matthes, Luís Pinto
Decidability of Several Concepts of Finiteness for Simple Types. Fundam. Informaticae 170 (1-3) (2019)
Ulrich Berger, Ralph Matthes, Anton Setzer
Martin Hofmann's Case for Non-Strictly Positive Data Types. TYPES (2018)
David Baelde, Arnaud Carayol, Ralph Matthes, Igor Walukiewicz
Preface. Fundam. Informaticae 150 (3-4) (2017)
Benedikt Ahrens, Ralph Matthes
Heterogeneous substitution systems revisited. CoRR (2016)
José Espírito Santo, Ralph Matthes, Luís Pinto
A Coinductive Approach to Proof Search through Typed Lambda-Calculi. CoRR (2016)
Benedikt Ahrens, Ralph Matthes, Anders Mörtberg
From signatures to monads in UniMath. CoRR (2016)
José Espírito Santo, Ralph Matthes, Luís Pinto
Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search. CoRR (2016)
Benedikt Ahrens, Ralph Matthes
Heterogeneous Substitution Systems Revisited. TYPES (2015)
José Espírito Santo, Ralph Matthes, Koji Nakazawa, Luís Pinto
Confluence for classical logic through the distinction between values and computations. CL&C (2014)
Ralph Matthes, Tarmo Uustalu
Preface. RAIRO Theor. Informatics Appl. 47 (1) (2013)
José Espírito Santo, Ralph Matthes, Luís Pinto
A Coinductive Approach to Proof Search. FICS (2013)
José Espírito Santo, Ralph Matthes, Koji Nakazawa, Luís Pinto
Monadic translation of classical sequent calculus. Math. Struct. Comput. Sci. 23 (6) (2013)
Mathias Winckel, Ralph Matthes
On a Dynamic Logic for Graph Rewriting. ICTERI (2013)
Ralph Matthes, Sergei Soloviev
Preface to the special issue: commutativity of algebraic diagrams. Math. Struct. Comput. Sci. 22 (6) (2012)
Célia Picard, Ralph Matthes
Permutations in Coinductive Graph Representation. CMCS (2012)
Ralph Matthes, Célia Picard
Verification of redecoration for infinite triangular matrices using coinduction. TYPES (2011)
Ralph Matthes
Map fusion for nested datatypes in intensional type theory. Sci. Comput. Program. 76 (3) (2011)
Célia Picard, Ralph Matthes
Coinductive Graph Representation: the Problem of Embedded Lists. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 39 (2011)
Mathieu Giorgino, Martin Strecker, Ralph Matthes, Marc Pantel
Verification of the Schorr-Waite Algorithm - From Trees to Graphs. LOPSTR (2010)
Ralph Matthes
An induction principle for nested datatypes in intensional type theory. J. Funct. Program. 19 (3-4) (2009)
José Espírito Santo, Ralph Matthes, Luís Pinto
Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi Log. Methods Comput. Sci. 5 (2) (2009)
José Espírito Santo, Ralph Matthes, Luís Pinto
Monadic Translation of Intuitionistic Sequent Calculus. TYPES (2008)
Ralph Matthes
Nested Datatypes with Generalized Mendler Iteration: Map Fusion and the Example of the Representation of Untyped Lambda Calculus with Explicit Flattening. MPC (2008)
Ralph Matthes, Sergei Soloviev
Preface to the special issue: isomorphisms of types and invertibility of lambda terms. Math. Struct. Comput. Sci. 18 (4) (2008)
Ralph Matthes
Recursion on Nested Datatypes in Dependent Type Theory. CiE (2008)
José Espírito Santo, Ralph Matthes, Luís Pinto
Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi. TLCA (2007)
Ralph Matthes, Martin Strecker
Verification of the Redecoration Algorithm for Triangular Matrices. TYPES (2007)
Ralph Matthes
A Datastructure for Iterated Powers. MPC (2006)
Ralph Matthes
Verification of Programs on Truly Nested Datatypes in Intensional Type Theory. MSFP@MPC (2006)
Andreas Abel, Ralph Matthes, Tarmo Uustalu
Iteration and coiteration schemes for higher-order and nested datatypes. Theor. Comput. Sci. 333 (1-2) (2005)
Ralph Matthes
Non-strictly positive fixed points for classical natural deduction. Ann. Pure Appl. Log. 133 (1-3) (2005)
Ralph Matthes, Tarmo Uustalu
Substitution in non-wellfounded syntax with variable binding. Theor. Comput. Sci. 327 (1-2) (2004)
Andreas Abel, Ralph Matthes
Fixed Points of Type Constructors and Primitive Recursion. CSL (2004)
Andreas Abel, Ralph Matthes
Primitive Recursion for Rank-2 Inductive Types. FICS (2003)
Ralph Matthes, Tarmo Uustalu
Substitution in Non-wellfounded Syntax with Variable Binding. CMCS (2003)
Andreas Abel, Ralph Matthes, Tarmo Uustalu
Generalized Iteration and Coiteration for Higher-Order Nested Datatypes. FoSSaCS (2003)
Felix Joachimski, Ralph Matthes
Short proofs of normalization for the simply- typed lambda-calculus, permutative conversions and Go"del's T. Arch. Math. Log. 42 (1) (2003)
Andreas Abel, Ralph Matthes
(Co-)Iteration for Higher-Order Nested Datatypes. TYPES (2002)
Ralph Matthes
Tarski's Fixed-Point Theorem And Lambda Calculi With Monotone Inductive Types. Synth. 133 (1-2) (2002)
Ralph Matthes
Interpolation for Natural Deduction with Generalized Eliminations. Proof Theory in Computer Science (2001)
Ralph Matthes
Parigot's Second Order lambda-mu-Calculus and Inductive Types. TLCA (2001)
Ralph Matthes
Monotone Inductive and Coinductive Constructors of Rank 2. CSL (2001)
Ralph Matthes
Characterizing Strongly Normalizing Terms of a Calculus with Generalized Applications via Intersection Types. ICALP Satellite Workshops (2000)
Felix Joachimski, Ralph Matthes
Standardization and Confluence for a Lambda Calculus with Generalized Applications. RTA (2000)
Ralph Matthes
Monotone (co)inductive types and positive fixed-point types. RAIRO Theor. Informatics Appl. 33 (4/5) (1999)
Ralph Matthes
Monotone Fixed-Point Types and Strong Normalization. CSL (1998)

Ralph Matthes.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Ralph Matthes