3 results
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 […]
Published on August 2, 2022
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 proof that it is a congruence, and generalised the result to all languages complying with a suitable format. We propose a […]
Published on September 21, 2022
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 […]
Published on March 1, 2024