Related papers: An Introduction to Different Approaches to Initial…
Matching logic (ML) was developed by Grigore Ro\c{s}u and collaborators as a logic for defining the formal semantics of programming languages and for specifying and reasoning about the behavior of programs. These lecture notes present basic…
ULLER (Unified Language for LEarning and Reasoning) offers a unified first-order logic (FOL) syntax, enabling its knowledge bases to be used directly across a wide range of neurosymbolic systems. The original specification endows this…
Higher inductive types are a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very fruitful for the "synthetic" development of homotopy…
We present the formalization of a theory of syntax with bindings that has been developed and refined over the last decade to support several large formalization efforts. Terms are defined for an arbitrary number of constructors of varying…
Monads are a popular tool for the working functional programmer to structure effectful computations. This paper presents polymonads, a generalization of monads. Polymonads give the familiar monadic bind the more general type forall a,b. L a…
The purpose of this article is twofold. Firstly, we use the next-token probabilities given by a language model to explicitly define a category of texts in natural language enriched over the unit interval, in the sense of Bradley, Terilla,…
Let $\Lambda^{\ast}$ be the free monoid of (finite) words over a not necessarily finite alphabet $\Lambda$, which is equipped with some (partial) order. This ordering lifts to $\Lambda^{\ast}$, where it extends the divisibility ordering of…
Graded monads refine traditional monads using effect annotations in order to describe quantitatively the computational effects that a program can generate. They have been successfully applied to a variety of formal systems for reasoning…
Terms are a concise representation of tree structures. Since they can be naturally defined by an inductive type, they offer data structures in functional programming and mechanised reasoning with useful principles such as structural…
It is informally understood that the purpose of modal type constructors in programming calculi is to control the flow of information between types. In order to lend rigorous support to this idea, we study the category of classified sets, a…
We present new induction principles for the syntax of dependent type theories, which we call relative induction principles. The result of the induction principle relative to a functor F into the syntax is stable over the codomain of F. We…
This paper contributes to the techniques of topo-algebraic recognition for languages beyond the regular setting as they relate to logic on words. In particular, we provide a general construction on recognisers corresponding to adding one…
When programmers want to prove strong program invariants, they are usually faced with a choice between using theorem provers and using traditional programming languages. The former requires them to provide program proofs, which, for many…
The focus of these lecture notes is on abstract models and basic ideas and results that relate to the operational semantics of programming languages largely conceived. The approach is to start with an abstract description of the computation…
The bisimulation proof method can be enhanced by employing `bisimulations up-to' techniques. A comprehensive theory of such enhancements has been developed for first-order (i.e., CCS-like) labelled transition systems (LTSs) and…
MetaML-style metaprogramming languages allow programmers to construct, manipulate and run code. In the presence of higher-order references for code, ensuring type safety is challenging, as free variables can escape their binders. In this…
The problem of learning a minimal consistent model from a set of labeled sequences of symbols is addressed from a satisfiability modulo theories perspective. We present two encodings for deterministic finite automata and extend one of these…
In this course we introduce the main notions relative to the classical theory of modular forms. A complete treatise in a similar style can be found in the author's book joint with F. Str{\"o}mberg [1].
The overall goal of this paper is to investigate the theoretical foundations of algorithmic verification techniques for first order linear logic specifications. The fragment of linear logic we consider in this paper is based on the linear…
The starting point of algebraic language theory is that regular languages of finite words are exactly those recognized by finite monoids. This finiteness condition gives rise to a topological space whose points, called profinite words,…