8 citations · 25 across the 12 of their papers we have counts for
7 papers · 1 filter
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…
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…