Ralph Matthes

According to our database, Ralph Matthes authored at least 52 papers between 1998 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

Displayed Monoidal Categories for the Semantics of Linear Logic.

Benedikt Ahrens, Ralph Matthes, Niels van der Weide, Kobe Wullaert

Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2024

2023

Substitution for Non-Wellfounded Syntax with Binders.

Ralph Matthes, Kobe Wullaert, Benedikt Ahrens

CoRR, 2023

Formalizing Monoidal Categories and Actions for Syntax with Binders.

Benedikt Ahrens, Ralph Matthes, Kobe Wullaert

CoRR, 2023

2022

Univalent Monoidal Categories.

Kobe Wullaert, Ralph Matthes, Benedikt Ahrens

Proceedings of the 28th International Conference on Types for Proofs and Programs, 2022

Implementing a category-theoretic framework for typed abstract syntax.

Benedikt Ahrens, Ralph Matthes, Anders Mörtberg

Proceedings of the CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17, 2022

2021

A coinductive approach to proof search through typed lambda-calculi.

José Espírito Santo, Ralph Matthes, Luís Pinto

Ann. Pure Appl. Log., 2021

2020

Proof search for full intuitionistic propositional logic through a coinductive approach for polarized logic.

José Espírito Santo, Ralph Matthes, Luís Pinto

CoRR, 2020

Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic.

José Espírito Santo, Ralph Matthes, Luís Pinto

Proceedings of the 26th International Conference on Types for Proofs and Programs, 2020

2019

Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search.

José Espírito Santo, Ralph Matthes, Luís Pinto

Math. Struct. Comput. Sci., 2019

From Signatures to Monads in UniMath.

Benedikt Ahrens, Ralph Matthes, Anders Mörtberg

J. Autom. Reason., 2019

Decidability of Several Concepts of Finiteness for Simple Types.

José Espírito Santo, Ralph Matthes, Luís Pinto

Fundam. Informaticae, 2019

Certification of Breadth-First Algorithms by Extraction.

Dominique Larchey-Wendling, Ralph Matthes

Proceedings of the Mathematics of Program Construction - 13th International Conference, 2019

2018

Martin Hofmann's Case for Non-Strictly Positive Data Types.

Ulrich Berger, Ralph Matthes, Anton Setzer

Proceedings of the 24th International Conference on Types for Proofs and Programs, 2018

2017

Preface.

David Baelde, Arnaud Carayol, Ralph Matthes, Igor Walukiewicz

Fundam. Informaticae, 2017

2015

Heterogeneous Substitution Systems Revisited.

Benedikt Ahrens, Ralph Matthes

Proceedings of the 21st International Conference on Types for Proofs and Programs, 2015

2014

Confluence for classical logic through the distinction between values and computations.

José Espírito Santo, Ralph Matthes, Koji Nakazawa, Luís Pinto

Proceedings of the Proceedings Fifth International Workshop on Classical Logic and Computation, 2014

2013

Monadic translation of classical sequent calculus.

José Espírito Santo, Ralph Matthes, Koji Nakazawa, Luís Pinto

Math. Struct. Comput. Sci., 2013

Preface.

Ralph Matthes, Tarmo Uustalu

RAIRO Theor. Informatics Appl., 2013

A Coinductive Approach to Proof Search.

José Espírito Santo, Ralph Matthes, Luís Pinto

Proceedings of the Proceedings Workshop on Fixed Points in Computer Science, 2013

On a Dynamic Logic for Graph Rewriting.

Mathias Winckel, Ralph Matthes

Proceedings of the 9th International Conference on ICT in Education, 2013

2012

Preface to the special issue: commutativity of algebraic diagrams.

Ralph Matthes, Sergei Soloviev

Math. Struct. Comput. Sci., 2012

Permutations in Coinductive Graph Representation.

Célia Picard, Ralph Matthes

Proceedings of the Coalgebraic Methods in Computer Science - 11th International Workshop, 2012

2011

Map fusion for nested datatypes in intensional type theory.

Ralph Matthes

Sci. Comput. Program., 2011

Coinductive Graph Representation: the Problem of Embedded Lists.

Célia Picard, Ralph Matthes

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011

Verification of redecoration for infinite triangular matrices using coinduction.

Ralph Matthes, Célia Picard

Proceedings of the 18th International Workshop on Types for Proofs and Programs, 2011

2010

Verification of the Schorr-Waite Algorithm - From Trees to Graphs.

Mathieu Giorgino, Martin Strecker, Ralph Matthes, Marc Pantel

Proceedings of the Logic-Based Program Synthesis and Transformation, 2010

2009

An induction principle for nested datatypes in intensional type theory.

Ralph Matthes

J. Funct. Program., 2009

Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi

José Espírito Santo, Ralph Matthes, Luís Pinto

Log. Methods Comput. Sci., 2009

2008

Preface to the special issue: isomorphisms of types and invertibility of lambda terms.

Ralph Matthes, Sergei Soloviev

Math. Struct. Comput. Sci., 2008

Monadic Translation of Intuitionistic Sequent Calculus.

José Espírito Santo, Ralph Matthes, Luís Pinto

Proceedings of the Types for Proofs and Programs, International Conference, 2008

Nested Datatypes with Generalized Mendler Iteration: Map Fusion and the Example of the Representation of Untyped Lambda Calculus with Explicit Flattening.

Ralph Matthes

Proceedings of the Mathematics of Program Construction, 9th International Conference, 2008

Recursion on Nested Datatypes in Dependent Type Theory.

Ralph Matthes

Proceedings of the Logic and Theory of Algorithms, 2008

2007

Verification of the Redecoration Algorithm for Triangular Matrices.

Ralph Matthes, Martin Strecker

Proceedings of the Types for Proofs and Programs, International Conference, 2007

2006

Verification of Programs on Truly Nested Datatypes in Intensional Type Theory.

Ralph Matthes

Proceedings of the Workshop on Mathematically Structured Functional Programming, 2006

A Datastructure for Iterated Powers.

Ralph Matthes

Proceedings of the Mathematics of Program Construction, 8th International Conference, 2006

2005

Iteration and coiteration schemes for higher-order and nested datatypes.

Andreas Abel, Ralph Matthes, Tarmo Uustalu

Theor. Comput. Sci., 2005

Non-strictly positive fixed points for classical natural deduction.

Ralph Matthes

Ann. Pure Appl. Log., 2005

2004

Fixed Points of Type Constructors and Primitive Recursion.

Andreas Abel, Ralph Matthes

Proceedings of the Computer Science Logic, 18th International Workshop, 2004

2003

Substitution in Non-wellfounded Syntax with Variable Binding.

Ralph Matthes, Tarmo Uustalu

Proceedings of the 6th International Workshop on Coalgebraic Methods in Computer Science, 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

Generalized Iteration and Coiteration for Higher-Order Nested Datatypes.

Andreas Abel, Ralph Matthes, Tarmo Uustalu

Proceedings of the Foundations of Software Science and Computational Structures, 2003

Primitive Recursion for Rank-2 Inductive Types.

Andreas Abel, Ralph Matthes

Proceedings of the FICS '03, 2003

2002

Tarski's Fixed-Point Theorem And Lambda Calculi With Monotone Inductive Types.

Ralph Matthes

Synth., 2002

(Co-)Iteration for Higher-Order Nested Datatypes.

Andreas Abel, Ralph Matthes

Proceedings of the Types for Proofs and Programs, Second International Workshop, 2002

2001

Parigot's Second Order lambda-mu-Calculus and Inductive Types.

Ralph Matthes

Proceedings of the Typed Lambda Calculi and Applications, 5th International Conference, 2001

Interpolation for Natural Deduction with Generalized Eliminations.

Ralph Matthes

Proceedings of the Proof Theory in Computer Science, International Seminar, 2001

Monotone Inductive and Coinductive Constructors of Rank 2.

Ralph Matthes

Proceedings of the Computer Science Logic, 15th International Workshop, 2001

2000

Standardization and Confluence for a Lambda Calculus with Generalized Applications.

Felix Joachimski, Ralph Matthes

Proceedings of the Rewriting Techniques and Applications, 11th International Conference, 2000

Characterizing Strongly Normalizing Terms of a Calculus with Generalized Applications via Intersection Types.

Ralph Matthes

Proceedings of the ICALP Workshops 2000, 2000

1999

Extensions of system F by iteration and primitive recursion on monotone inductive types.

Ralph Matthes

PhD thesis, 1999

Monotone (co)inductive types and positive fixed-point types.

Ralph Matthes

RAIRO Theor. Informatics Appl., 1999

1998

Monotone Fixed-Point Types and Strong Normalization.

Ralph Matthes

Proceedings of the Computer Science Logic, 12th International Workshop, 1998