Abstract We propose a notion of syntax with metavariables that generalises Miller’s decidable pattern fragment of second-order unification for simply typed $\lambda$ -calculus. Using categorical semantics, we show that, under some conditions, a generalisation of Miller’s unification algorithm applies. To illustrate our semantic analysis, we implemented our generic unification algorithm in Agda. The syntax with metavariables given as input of the algorithm is specified by a notion of signature generalising binding signatures, covering a wide range of examples, including ordered $\lambda$ -calculus and (intrinsic) polymorphic syntax such as System F. Although we do not explicitly handle equations, we also tackle simply typed $\lambda$ -calculus modulo $\beta$ - and $\eta$ -equations (Miller’s original setting) by working on the syntax of normal forms.

Initial semantics aims to model inductive structures and their properties, and to provide them with recursion principles respecting these properties. An ubiquitous example is the fold operator for lists. We are concerned with initial semantics that model languages with variable binding and their substitution structure, and that provide substitution-safe recursion principles. There are different approaches to implementing languages with variable binding depending on the choice of representation for contexts and free variables, such as unscoped syntax, or well-scoped syntax with finite or infinite contexts. Abstractly, each approach corresponds to choosing a different monoidal category to model contexts and binding, each choice yielding a different notion of “model” for the same abstract specification (or “signature”). In this work, we provide tools to compare and relate the models obtained from a signature for different choices of monoidal category. We do so by showing that initial semantics naturally has a 2-categorical structure when parametrized by the monoidal category modeling contexts. We thus can relate models obtained from different choices of monoidal categories provided the monoidal categories themselves are related. In particular, we use our results to relate the models of the different implementation — de Bruijn vs locally nameless, finite vs infinite contexts —, and to provide a generalized recursion principle for simply-typed syntax.

By abstracting over well-known properties of De Bruijn's representation with nameless dummies, we design a new theory of syntax with variable binding and capture-avoiding substitution. We propose it as a simpler alternative to Fiore, Plotkin, and Turi's approach, with which we establish a strong formal link. We also show that our theory easily incorporates simple types and equations between terms.

Systems programmers need fine-grained control over the memory layout of data structures, both to produce performant code and to comply with well-defined interfaces imposed by existing code, standardised protocols or hardware. Code that manipulates these low-level representations in memory is hard to get right. Traditionally, this problem is addressed by the implementation of tedious marshalling code to convert between compiler-selected data representations and the desired compact data formats. Such marshalling code is error-prone and can lead to a significant runtime overhead due to excessive copying. While there are many languages and systems that address the correctness issue, by automating the generation and, in some cases, the verification of the marshalling code, the performance overhead introduced by the marshalling code remains. In particular for systems code, this overhead can be prohibitive. In this work, we address both the correctness and the performance problems. We present a data layout description language and data refinement framework, called Dargent, which allows programmers to declaratively specify how algebraic data types are laid out in memory. Our solution is applied to the Cogent language, but the general ideas behind our solution are applicable to other settings. The Dargent framework generates C code that manipulates data directly with the desired memory layout, while retaining the formal proof that this generated C code is correct with respect to the functional semantics. This added expressivity removes the need for implementing and verifying marshalling code, which eliminates copying, smoothens interoperability with surrounding systems, and increases the trustworthiness of the overall system.

Abstract By abstracting over well-known properties of De Bruijn’s representation with nameless dummies, we design a new theory of syntax with variable binding and capture-avoiding substitution. We propose it as a simpler alternative to Fiore, Plotkin, and Turi’s approach, with which we establish a strong formal link. We also show that our theory easily incorporates simple types and equations between terms.

This paper is a contribution to the search for efficient and high-level mathematical tools to specify and reason about (abstract) programming languages or calculi. Generalising the reduction monads of Ahrens et al., we introduce transition monads, thus covering new applications such as lambda-bar-mu-calculus, pi-calculus, Positive GSOS specifications, differential lambda-calculus, and the big-step, simply-typed, call-by-value lambda-calculus. Moreover, we design a suitable notion of signature for transition monads.

Applicative bisimilarity is a coinductive characterisation of observational equivalence in call-by-name lambda-calculus, introduced by Abramsky (1990). Howe (1996) gave a direct proof that it is a congruence, and generalised the result to all languages complying with a suitable format. We propose a categorical framework for specifying operational semantics, in which we prove that (an abstract analogue of) applicative bisimilarity is automatically a congruence. Example instances include standard applicative bisimilarity in call-by-name, call-by-value, and call-by-name non-deterministic $\lambda$-calculus, and more generally all languages complying with a variant of Howe's format.

This paper is a contribution to the search for efficient and high-level mathematical tools to specify and reason about (abstract) programming languages or calculi. Generalising the reduction monads of Ahrens et al., we introduce transition monads, thus covering new applications such as ̅λμ-calculus, π-calculus, Positive GSOS specifications, differential λ-calculus, and the big-step, simply-typed, call-by-value λ-calculus. Finally, we design a suitable notion of signature for transition monads.

We introduce a categorical framework for operational semantics, in which we define substitution-closed bisimilarity, an abstract analogue of the open extension of Abramsky's applicative bisimilarity. We furthermore prove a congruence theorem for substitution-closed bisimilarity, following Howe's method. We finally demonstrate that the framework covers the call-by-name and call-by-value variants of λ-calculus in big-step style. As an intermediate result, we generalise the standard framework of Fiore et al. for syntax with variable binding to the skew-monoidal case.

In this work, we study reduction monads , which are essentially the same as monads relative to the free functor from sets into multigraphs. Reduction monads account for two aspects of the lambda calculus: on the one hand, in the monadic viewpoint, the lambda calculus is an object equipped with a well-behaved substitution; on the other hand, in the graphical viewpoint, it is an oriented multigraph whose vertices are terms and whose edges witness the reductions between two terms. We study presentations of reduction monads. To this end, we propose a notion of reduction signature . As usual, such a signature plays the role of a virtual presentation, and specifies arities for generating operations—possibly subject to equations—together with arities for generating reduction rules. For each such signature, we define a category of models; any model is, in particular, a reduction monad. If the initial object of this category of models exists, we call it the reduction monad presented (or specified) by the given reduction signature . Our main result identifies a class of reduction signatures which specify a reduction monad in the above sense. We show in the examples that our approach covers several standard variants of the lambda calculus.

We present a device for specifying and reasoning about syntax for datatypes, programming languages, and logic calculi. More precisely, we consider a general notion of "signature" for specifying syntactic constructions. Our signatures subsume classical algebraic signatures (i.e., signatures for languages with variable binding, such as the pure lambda calculus) and extend to much more general examples. In the spirit of Initial Semantics, we define the "syntax generated by a signature" to be the initial object - if it exists - in a suitable category of models. Our notions of signature and syntax are suited for compositionality and provide, beyond the desired algebra of terms, a well-behaved substitution and the associated inductive/recursive principles. Our signatures are "general" in the sense that the existence of an associated syntax is not automatically guaranteed. In this work, we identify a large and simple class of signatures which do generate a syntax. This paper builds upon ideas from a previous attempt by Hirschowitz-Maggesi, which, in turn, was directly inspired by some earlier work of Ghani-Uustalu-Hamana and Matthes-Uustalu. The main results presented in the paper are computer-checked within the UniMath system.