Ralph Matthes

Available identifiers

zbMath Open matthes.ralphMaRDI QIDQ627203

List of research outcomes

Publication	Date of Publication	Type
Formalizing Monoidal Categories and Actions for Syntax with Binders	2023-07-30	Paper
Univalent Monoidal Categories	2022-12-06	Paper
Martin Hofmann's Case for Non-Strictly Positive Data Types	2022-07-21	Paper
Implementing a Category-Theoretic Framework for Typed Abstract Syntax	2021-12-13	Paper
A coinductive approach to proof search through typed lambda-calculi	2021-09-30	Paper
https://portal.mardi4nfdi.de/entity/Q4995381	2021-06-24	Paper
https://portal.mardi4nfdi.de/entity/Q4992896	2021-06-10	Paper
Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic	2020-07-31	Paper
Certification of breadth-first algorithms by extraction	2020-05-05	Paper
Decidability of Several Concepts of Finiteness for Simple Types	2020-01-24	Paper
Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search	2019-10-09	Paper
From signatures to monads in \textsf{UniMath}	2019-08-21	Paper
Heterogeneous Substitution Systems Revisited	2018-08-13	Paper
https://portal.mardi4nfdi.de/entity/Q2957696	2017-01-27	Paper
A Coinductive Approach to Proof Search through Typed Lambda-Calculi	2016-02-13	Paper
Monadic translation of classical sequent calculus	2014-04-16	Paper
https://portal.mardi4nfdi.de/entity/Q2843728	2013-08-23	Paper
Permutations in Coinductive Graph Representation	2012-09-20	Paper
Verification of the Schorr-Waite Algorithm – From Trees to Graphs	2011-05-27	Paper
Map fusion for nested datatypes in intensional type theory	2011-02-21	Paper
An induction principle for nested datatypes in intensional type theory	2009-10-28	Paper
Monadic Translation of Intuitionistic Sequent Calculus	2009-07-02	Paper
Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi	2009-06-30	Paper
A Datastructure for Iterated Powers	2009-04-02	Paper
Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi	2009-03-10	Paper
Nested Datatypes with Generalized Mendler Iteration: Map Fusion and the Example of the Representation of Untyped Lambda Calculus with Explicit Flattening	2008-08-28	Paper
Recursion on Nested Datatypes in Dependent Type Theory	2008-06-19	Paper
Verification of the Redecoration Algorithm for Triangular Matrices	2008-06-03	Paper
https://portal.mardi4nfdi.de/entity/Q5477358	2006-07-03	Paper
Computer Science Logic	2005-08-22	Paper
Non-strictly positive fixed points for classical natural deduction	2005-04-21	Paper
Iteration and coiteration schemes for higher-order and nested datatypes	2005-04-06	Paper
Substitution in non-wellfounded syntax with variable binding	2005-01-11	Paper
https://portal.mardi4nfdi.de/entity/Q4436032	2003-11-23	Paper
https://portal.mardi4nfdi.de/entity/Q4435457	2003-11-12	Paper
Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)	2003-09-16	Paper
https://portal.mardi4nfdi.de/entity/Q4417851	2003-07-30	Paper
Tarski's fixed-point theorem and lambda calculi with monotone inductive types	2003-04-27	Paper
https://portal.mardi4nfdi.de/entity/Q4783334	2002-12-04	Paper
A locally trivial quantum Hopf bundle	2002-10-14	Paper
https://portal.mardi4nfdi.de/entity/Q2778830	2002-03-21	Paper
https://portal.mardi4nfdi.de/entity/Q2723897	2001-07-08	Paper
Monotone (co)inductive types and positive fixed-point types	2000-07-24	Paper
https://portal.mardi4nfdi.de/entity/Q4263804	2000-03-29	Paper
https://portal.mardi4nfdi.de/entity/Q4720069	2000-01-09	Paper

Research outcomes over time

Doctoral students

No records found.

Known relations from the MaRDI Knowledge Graph

Property	Value
MaRDI profile type	MaRDI person profile
instance of	human

This page was built for person: Ralph Matthes