9 citations · 26 across the 9 of their papers we have counts for
12 papers
Substitution for Non-Wellfounded Syntax with Binders through Monoidal Categories
Ralph Matthes, Kobe Wullaert, Benedikt Ahrens
We describe a generic construction of non-wellfounded syntax involving variable binding and its monadic substitution operation. Our construction of the syntax and its substitution…
Formalizing Monoidal Categories and Actions for Syntax with Binders
Benedikt Ahrens, Ralph Matthes, Kobe Wullaert
We discuss some aspects of our work on the mechanization of syntax and semantics in the UniMath library, based on the proof assistant Coq. We focus on experiences where Coq (as a t…
Univalent Monoidal Categories
Kobe Wullaert, Ralph Matthes, Benedikt Ahrens
Univalent categories constitute a well-behaved and useful notion of category in univalent foundations. The notion of univalence has subsequently been generalized to bicategories an…
Implementing a Category-Theoretic Framework for Typed Abstract Syntax
Benedikt Ahrens, Ralph Matthes, Anders Mörtberg
In previous work ("From signatures to monads in UniMath"), we described a category-theoretic construction of abstract syntax from a signature, mechanized in the UniMath library bas…
Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic
José Espírito Santo, Ralph Matthes, Luís Pinto
The approach to proof search dubbed "coinductive proof search" (CoIPS), and previously developed by the authors for implicational intuitionistic logic, is in this paper extended to…
From signatures to monads in UniMath
Benedikt Ahrens, Ralph Matthes, Anders Mörtberg
The term UniMath refers both to a formal system for mathematics, as well as a computer-checked library of mathematics formalized in that system. The UniMath system is a core depend…
Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search
José Espírito Santo, Ralph Matthes, Luís Pinto
A new, comprehensive approach to inhabitation problems in simply-typed lambda-calculus is shown, dealing with both decision and counting problems. This approach works by exploiting…
A Coinductive Approach to Proof Search through Typed Lambda-Calculi
José Espírito Santo, Ralph Matthes, Luís Pinto
In reductive proof search, proofs are naturally generalized by solutions, comprising all possibly infinite structures generated by locally correct, bottom-up application of inferen…
Proceedings Tenth International Workshop on Fixed Points in Computer Science
Ralph Matthes, Matteo Mio
This volume contains the proceedings of the Tenth International Workshop on Fixed Points in Computer Science (FICS 2015) which took place on September 11th and 12th, 2015 in Berlin…
Confluence for classical logic through the distinction between values and computations
José Espírito Santo, Ralph Matthes, Koji Nakazawa +1
We apply an idea originated in the theory of programming languages - monadic meta-language with a distinction between values and computations - in the design of a calculus of cut-e…
A Coinductive Approach to Proof Search
José Espírito Santo, Ralph Matthes, Luís Pinto
We propose to study proof search from a coinductive point of view. In this paper, we consider intuitionistic logic and a focused system based on Herbelin's LJT for the implicationa…
Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi
Jose Espirito Santo, Ralph Matthes, Luis Pinto
The intuitionistic fragment of the call-by-name version of Curien and Herbelin's λ\_mu\_{mu}-calculus is isolated and proved strongly normalising by means of an embedding into the…