8 citations · 25 across the 12 of their papers we have counts for
12 papers
For Generalised Algebraic Theories, Two Sorts Are Enough
Samy Avrillon, Ambrus Kaposi, Ambroise Lafont +2
Generalised algebraic theories (GATs) allow multiple sorts indexed over each other. For example, the theories of categories or Martin-L{ö}f type theories form GATs. Categories have…
2-Functoriality of Initial Semantics, and Applications
Benedikt Ahrens, Ambroise Lafont, Thomas Lamiaux
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 f…
A more general categorical framework for congruence of applicative bisimilarity
Tom Hirschowitz, Ambroise Lafont
We prove a general congruence result for bisimilarity in higher-order languages, which generalises previous work to languages specified by a labelled transition system in which pro…
Variable binding and substitution for (nameless) dummies
André Hirschowitz, Tom Hirschowitz, Ambroise Lafont +1
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 substitut…
A unified treatment of structural definitions on syntax for capture-avoiding substitution, context application, named substitution, partial differentiation, and so on
Tom Hirschowitz, Ambroise Lafont
We introduce a category-theoreticabstraction of a syntax with auxiliary functions, called an admissiblemonad morphism. Relying on an abstract form of structural recursion,we then d…
A categorical framework for congruence of applicative bisimilarity in higher-order languages
Tom Hirschowitz, Ambroise Lafont
Applicative bisimilarity is a coinductive characterisation of observational equivalence in call-by-name lambda-calculus, introduced by Abramsky (1990). Howe (1996) gave a direct pr…
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 and Their Signatures
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont +1
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 aspect…
Signatures and models for syntax and operational semantics in the presence of variable binding
Ambroise Lafont
This thesis deals with the specification and construction of syntax and operational semantics of a programming language. We work with a general notion of signature for specifying o…
Modular specification of monads through higher-order presentations
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont +1
In their work on second-order equational logic, Fiore and Hur have studied presentations of simply typed languages by generating binding constructions and equations among them. To…
Presentable signatures and initial semantics
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont +1
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 specifyi…
Probing wave function collapse models with a classically driven mechanical oscillator
Melvyn Ho, Ambroise Lafont, Nicolas Sangouard +1
We show that the interaction of a pulsed laser light with a mechanical oscillator through the radiation pressure results in an opto-mechanical entangled state in which the photon n…