Search

• < Previous
• 1
• Next >

---

Presentable signatures and initial semantics

Benedikt Ahrens ; André Hirschowitz ; Ambroise Lafont ; Marco Maggesi.

We present a device for specifying and reasoning about syntax for datatypes, programming languages, and logic calculi. More precisely, we study a notion of "signature" for specifying syntactic constructions. In the spirit of Initial Semantics, we define the "syntax generated by a signature" to be&nbsp;[&hellip;]

---

Modules over monads and operational semantics (expanded version)

André Hirschowitz ; Tom Hirschowitz ; Ambroise Lafont.

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&nbsp;[&hellip;]

---

Variable binding and substitution for (nameless) dummies

André Hirschowitz ; Tom Hirschowitz ; Ambroise Lafont ; Marco Maggesi.

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&nbsp;[&hellip;]

---