Document

**Published in:** LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

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 takes place in category theory, notably by using monoidal categories and strong functors between them. A language is specified by a multi-sorted binding signature, say Σ. First, we provide sufficient criteria for Σ to generate a language of possibly infinite terms, through ω-continuity. Second, we construct a monadic substitution operation for the language generated by Σ. A cornerstone in this construction is a mild generalization of the notion of heterogeneous substitution systems developed by Matthes and Uustalu; such a system encapsulates the necessary corecursion scheme for implementing substitution.
The results are formalized in the Coq proof assistant, through the UniMath library of univalent mathematics.

Ralph Matthes, Kobe Wullaert, and Benedikt Ahrens. Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 25:1-25:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{matthes_et_al:LIPIcs.FSCD.2024.25, author = {Matthes, Ralph and Wullaert, Kobe and Ahrens, Benedikt}, title = {{Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {25:1--25:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.25}, URN = {urn:nbn:de:0030-drops-203540}, doi = {10.4230/LIPIcs.FSCD.2024.25}, annote = {Keywords: Non-wellfounded syntax, Substitution, Monoidal categories, Actegories, Tensorial strength, Proof assistant Coq, UniMath library} }

Document

**Published in:** LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

Univalent categories constitute a well-behaved and useful notion of category in univalent foundations. The notion of univalence has subsequently been generalized to bicategories and other structures in (higher) category theory. Here, we zoom in on monoidal categories and study them in a univalent setting. Specifically, we show that the bicategory of univalent monoidal categories is univalent. Furthermore, we construct a Rezk completion for monoidal categories: we show how any monoidal category is weakly equivalent to a univalent monoidal category, universally. We have fully formalized these results in UniMath, a library of univalent mathematics in the Coq proof assistant.

Kobe Wullaert, Ralph Matthes, and Benedikt Ahrens. Univalent Monoidal Categories. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 15:1-15:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{wullaert_et_al:LIPIcs.TYPES.2022.15, author = {Wullaert, Kobe and Matthes, Ralph and Ahrens, Benedikt}, title = {{Univalent Monoidal Categories}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {15:1--15:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-285-3}, ISSN = {1868-8969}, year = {2023}, volume = {269}, editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.15}, URN = {urn:nbn:de:0030-drops-184580}, doi = {10.4230/LIPIcs.TYPES.2022.15}, annote = {Keywords: Univalence, Monoidal categories, Rezk completion, Displayed (bi)categories, Proof assistant Coq, UniMath library} }

Document

**Published in:** LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)

The approach to proof search dubbed "coinductive proof search", and previously developed by the authors for implicational intuitionistic logic, is in this paper extended to LJP, a focused sequent-calculus presentation of polarized intuitionistic logic, including an array of positive and negative connectives. As before, this includes developing a coinductive description of the search space generated by a sequent, an equivalent inductive syntax describing the same space, and decision procedures for inhabitation problems in the form of predicates defined by recursion on the inductive syntax. We prove the decidability of existence of focused inhabitants, and of finiteness of the number of focused inhabitants for polarized intuitionistic logic, by means of such recursive procedures. Moreover, the polarized logic can be used as a platform from which proof search for other logics is understood. We illustrate the technique with LJT, a focused sequent calculus for full intuitionistic propositional logic (including disjunction). For that, we have to work out the "negative translation" of LJT into LJP (that sees all intuitionistic types as negative types), and verify that the translation gives a faithful representation of proof search in LJT as proof search in the polarized logic. We therefore inherit decidability of both problems studied for LJP and thus get new proofs of these results for LJT.

José Espírito Santo, Ralph Matthes, and Luís Pinto. Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 4:1-4:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{espiritosanto_et_al:LIPIcs.TYPES.2020.4, author = {Esp{\'\i}rito Santo, Jos\'{e} and Matthes, Ralph and Pinto, Lu{\'\i}s}, title = {{Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic}}, booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)}, pages = {4:1--4:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-182-5}, ISSN = {1868-8969}, year = {2021}, volume = {188}, editor = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.4}, URN = {urn:nbn:de:0030-drops-138837}, doi = {10.4230/LIPIcs.TYPES.2020.4}, annote = {Keywords: Inhabitation problems, Coinduction, Lambda-calculus, Polarized logic} }

Document

**Published in:** LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)

We describe the breadth-first traversal algorithm by Martin Hofmann that uses a non-strictly positive data type and carry out a simple verification in an extensional setting. Termination is shown by implementing the algorithm in the strongly normalising extension of system F by Mendler-style recursion. We then analyze the same algorithm by alternative verifications first in an intensional setting using a non-strictly positive inductive definition (not just a non-strictly positive data type), and subsequently by two different algebraic reductions. The verification approaches are compared in terms of notions of simulation and should elucidate the somewhat mysterious algorithm and thus make a case for other uses of non-strictly positive data types. Except for the termination proof, which cannot be formalised in Coq, all proofs were formalised in Coq and some of the algorithms were implemented in Agda and Haskell.

Ulrich Berger, Ralph Matthes, and Anton Setzer. Martin Hofmann’s Case for Non-Strictly Positive Data Types. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 1:1-1:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{berger_et_al:LIPIcs.TYPES.2018.1, author = {Berger, Ulrich and Matthes, Ralph and Setzer, Anton}, title = {{Martin Hofmann’s Case for Non-Strictly Positive Data Types}}, booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)}, pages = {1:1--1:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-106-1}, ISSN = {1868-8969}, year = {2019}, volume = {130}, editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.1}, URN = {urn:nbn:de:0030-drops-114052}, doi = {10.4230/LIPIcs.TYPES.2018.1}, annote = {Keywords: non strictly-positive data types, breadth-first traversal, program verification, Mendler-style recursion, System F, theorem proving, Coq, Agda, Haskell} }

Document

**Published in:** LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)

Matthes and Uustalu (TCS 327(1--2):155--174, 2004) presented a
categorical description of substitution systems capable of capturing
syntax involving binding which is independent of whether the syntax
is made up from least or greatest fixed points.
We extend this work
in two directions: we continue the analysis by creating more
categorical structure, in particular by organizing substitution
systems into a category and studying its properties, and we develop
the proofs of the results of the cited paper and our new ones in
UniMath, a recent library of univalent mathematics formalized in the Coq theorem
prover.

Benedikt Ahrens and Ralph Matthes. Heterogeneous Substitution Systems Revisited. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 2:1-2:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{ahrens_et_al:LIPIcs.TYPES.2015.2, author = {Ahrens, Benedikt and Matthes, Ralph}, title = {{Heterogeneous Substitution Systems Revisited}}, booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)}, pages = {2:1--2:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-030-9}, ISSN = {1868-8969}, year = {2018}, volume = {69}, editor = {Uustalu, Tarmo}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.2}, URN = {urn:nbn:de:0030-drops-84724}, doi = {10.4230/LIPIcs.TYPES.2015.2}, annote = {Keywords: formalization of category theory, nested datatypes, Mendler-style recursion schemes, representation of substitution in languages with variable binding} }

Document

Complete Volume

**Published in:** LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)

LIPIcs, Volume 26, TYPES'13, Complete Volume

19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Proceedings{matthes_et_al:LIPIcs.TYPES.2013, title = {{LIPIcs, Volume 26, TYPES'13, Complete Volume}}, booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-72-9}, ISSN = {1868-8969}, year = {2014}, volume = {26}, editor = {Matthes, Ralph and Schubert, Aleksy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013}, URN = {urn:nbn:de:0030-drops-46370}, doi = {10.4230/LIPIcs.TYPES.2013}, annote = {Keywords: Applicative (Functional) Programming, Software/Program Verification, Specifying and Verifying and Reasoning about Programs, Mathematical Logic} }

Document

Front Matter

**Published in:** LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)

Frontmatter, Table of Contents, Preface, Conference Organization

19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. i-x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{matthes_et_al:LIPIcs.TYPES.2013.i, author = {Matthes, Ralph and Schubert, Aleksy}, title = {{Frontmatter, Table of Contents, Preface, Conference Organization}}, booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)}, pages = {i--x}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-72-9}, ISSN = {1868-8969}, year = {2014}, volume = {26}, editor = {Matthes, Ralph and Schubert, Aleksy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.i}, URN = {urn:nbn:de:0030-drops-46225}, doi = {10.4230/LIPIcs.TYPES.2013.i}, annote = {Keywords: Frontmatter, Table of Contents, Preface, Conference Organization} }

Document

**Published in:** LIPIcs, Volume 19, 18th International Workshop on Types for Proofs and Programs (TYPES 2011)

Finite triangular matrices with a dedicated type for the diagonal
elements can be profitably represented by a nested data type, i. e., a
heterogeneous family of inductive data types, while infinite
triangular matrices form an example of a nested coinductive type,
which is a heterogeneous family of coinductive data types.
Redecoration for infinite triangular matrices is taken up from
previous work involving the first author, and it is shown that
redecoration forms a comonad with respect to bisimilarity.
The main result, however, is a validation of the original algorithm
against a model based on infinite streams of infinite streams. The
two formulations are even provably equivalent, and the second is
identified as a special instance of the generic cobind operation
resulting from the well-known comultiplication operation on streams
that creates the stream of successive tails of a given stream. Thus,
perhaps surprisingly, the verification of redecoration is easier for
infinite triangular matrices than for their finite counterpart.
All the results have been obtained and are fully formalized in the
current version of the Coq theorem proving environment where these
coinductive datatypes are fully supported since the version 8.1,
released in 2007. Nonetheless, instead of displaying the Coq
development, we have chosen to write the paper in standard
mathematical and type-theoretic language. Thus, it should be
accessible without any specific knowledge about Coq.

Ralph Matthes and Celia Picard. Verification of redecoration for infinite triangular matrices using coinduction. In 18th International Workshop on Types for Proofs and Programs (TYPES 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 19, pp. 55-69, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{matthes_et_al:LIPIcs.TYPES.2011.55, author = {Matthes, Ralph and Picard, Celia}, title = {{Verification of redecoration for infinite triangular matrices using coinduction}}, booktitle = {18th International Workshop on Types for Proofs and Programs (TYPES 2011)}, pages = {55--69}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-49-1}, ISSN = {1868-8969}, year = {2013}, volume = {19}, editor = {Danielsson, Nils Anders and Nordstr\"{o}m, Bengt}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2011.55}, URN = {urn:nbn:de:0030-drops-39001}, doi = {10.4230/LIPIcs.TYPES.2011.55}, annote = {Keywords: nested datatype, coinduction, theorem proving, Coq} }