Ralph Matthes - RankMe

64 papers B 10C 2Misc 1Journal 28Unranked 19

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