Related papers: Nominal Algebraic-Coalgebraic Data Types, with App…
We define a type system with intersection types for an extension of lambda-calculus with unbind and rebind operators. In this calculus, a term with free variables, representing open code, can be packed into an "unbound" term, and passed…
Combinatorial design theory studies set systems with certain balance and symmetry properties and has applications to computer science and elsewhere. This paper presents a modular approach to formalising designs for the first time using…
Our goal is to define an algebraic language for reasoning about non-deterministic computations. Towards this goal, we introduce an algebra of string-to-string transductions. Specifically, it is an algebra of partial functions on words over…
A general overview of the existing difference ring theory for symbolic summation is given. Special emphasis is put on the user interface: the translation and back translation of the corresponding representations within the term algebra and…
We propose a categorial grammar based on classical multiplicative linear logic. This can be seen as an extension of abstract categorial grammars (ACG) and is at least as expressive. However, constituents of {\it linear logic grammars (LLG)}…
In this work, we study the notions of relative comonad and comodule over a relative comonad, and use these notions to give a terminal coalgebra semantics for the coinductive type families of streams and of infinite triangular matrices,…
We study what we call topological cylindric algebras and tense cylindric algebras defined for every ordinal $\alpha$. The former are cylindric algebras of dimension $\alpha$ expanded with $\sf S4$ modalities indexed by $\alpha$. The…
In this paper we present a framework for modelling \emph{reward-sensitive bisimulations}, that is, bisimulations that account for quantitative differences such as accumulated rewards. To capture both qualitative and quantitative aspects…
We bring forward a logical system of transition algebras that enhances many-sorted first-order logic using features from dynamic logics. The sentences we consider include compositions, unions, and transitive closures of transition…
Kurz et al. have recently shown that infinite $\lambda$-trees with finitely many free variables modulo $\alpha$-equivalence form a final coalgebra for a functor on the category of nominal sets. Here we investigate the rational fixpoint of…
We present the guarded lambda-calculus, an extension of the simply typed lambda-calculus with guarded recursive and coinductive types. The use of guarded recursive types ensures the productivity of well-typed programs. Guarded recursive…
The paper uses the formalism of indexed categories to recover the proof of a standard final coalgebra theorem, thus showing existence of final coalgebras for a special class of functors on categories with finite limits and colimits. As an…
These notes aim to provide a classical approach to solving some conformable differential equations based on prior knowledge of how to solve ordinary differential equations. That is, using the methods of separation of variables, homogeneous…
Computational reflection allows us to turn verified decision procedures into efficient automated reasoning tools in proof assistants. The typical applications of such methodology include mathematical structures that have decidable theory…
The algebraic method provides useful techniques to identify models in designs and to understand aliasing of polynomial models. The present note surveys the topic of Gr\"obner bases in experimental design and then describes the notion of…
Description Logics are knowledge representation formalisms that provide, for example, the logical underpinning of the W3C OWL standards. Conjunctive queries, the standard query language in databases, have recently gained significant…
We introduce a new representation of non-idempotent intersection types, using \textbf{sequences} (families indexed with natural numbers) instead of lists or multisets. This allows scaling up \textbf{intersection type} theory to the…
The operational semantics of interactive systems is usually described by labeled transition systems. Abstract semantics (that is defined in terms of bisimilarity) is characterized by the final morphism in some category of coalgebras. Since…
This paper provides a new categorification of the Lebesgue integral with variable upper limits by using normed modules over finite-dimensional $\Bbbk$-algebras $\mathit{\Lambda}$ and the category $\mathscr{A}^p_{\mathit{\Lambda}}$…
We derive "numerical" criteria for the existence of embeddings of representations of finite dimensional algebras.