Related papers: Substitution for Non-Wellfounded Syntax with Binde…
In this paper, a monad-based denotational model is introduced and shown adequate for the Proto-Quipper family of calculi, themselves being idealized versions of the Quipper programming language. The use of a monadic approach allows us to…
We introduce a general construction on 2-monads. We develop background on maps of 2-monads, their left semi-algebras, and colimits in 2-category. Then, we introduce the construction of a colimit induced by a map of 2-monads, show that we…
We introduce context-free languages of morphisms in monoidal categories, extending recent work on the categorification of context-free languages, and regular languages of string diagrams. Context-free languages of string diagrams include…
This paper considers the possible underlying multicategories for a symmetric monoidal category, and shows that, up to canonical and coherent isomorphism, there really is only one. As a result, there is a well-defined forgetful functor from…
Layered monoidal theories provide a categorical framework for studying scientific theories at different levels of abstraction, via string diagrammatic algebra. We introduce models for three closely related classes of layered monoidal…
Recent models of intensional type theory have been constructed in algebraic weak factorization systems (AWFSs). AWFSs give rise to comprehension categories that feature non-trivial morphisms between types; these morphisms are not used in…
In some bicategories, the 1-cells are `morphisms' between the 0-cells, such as functors between categories, but in others they are `objects' over the 0-cells, such as bimodules, spans, distributors, or parametrized spectra. Many…
Sharing of notations and theories across an inheritance hierarchy of mathematical structures, e.g., groups and rings, is important for productivity when formalizing mathematics in proof assistants. The packed classes methodology is a…
This paper describes an alternative method of generating fixed points of certain substitution systems. This method centres on taking infinite words consisting of one repeated letter per word. These infinite words are then interlaced to form…
When using interactive theorem provers based on dependent type theory to define and reason about languages involving binding constructs, we advocate the use of a well-scoped version of the locally nameless method of representing syntax.…
Inspired by the classical theory of modules over a monoid, we give a first account of the natural notion of module over a monad. The associated notion of morphism of left modules ("Linear" natural transformations) captures an important…
This tutorial gives an advanced introduction to string diagrams and graph languages for higher-order computation. The subject matter develops in a principled way, starting from the two dimensional syntax of key categorical concepts such as…
During the last decades, classical models in language theory have been extended by control mechanisms defined by monoids. We study which monoids cause the extensions of context-free grammars, finite automata, or finite state transducers to…
Applied category theory often studies symmetric monoidal categories (SMCs) whose morphisms represent open systems. These structures naturally accommodate complex wiring patterns, leveraging (co)monoidal structures for splitting and merging…
We introduce a universe of regular datatypes with variable binding information, for which we define generic formation and elimination (i.e. induction /recursion) operators. We then define a generic alpha-equivalence relation over the types…
Multi-adjoint logic programming is a general framework with interesting features, which involves other positive logic programming frameworks such as monotonic and residuated logic programming, generalized annotated logic programs, fuzzy…
The problem of identifying a probabilistic context free grammar has two aspects: the first is determining the grammar's topology (the rules of the grammar) and the second is estimating probabilistic weights for each rule. Given the hardness…
A number of domain specific languages, such as circuits or data-science workflows, are best expressed as diagrams of boxes connected by wires. Unfortunately, functional languages have traditionally been ill-equipped to embed this sort of…
The problem of identifying a probabilistic context free grammar has two aspects: the first is determining the grammar's topology (the rules of the grammar) and the second is estimating probabilistic weights for each rule. Given the hardness…
We define a bar construction endofunctor on the category of commutative augmented monoids $A$ of a symmetric monoidal category $\mathcal{V}$ endowed with a left adjoint monoidal functor $F:s\mathbf{Set}\to \mathcal{V}$. To do this, we need…