16 marca 2017 10:00
Maciej Piróg: Syntax and Handlers for Operations with Scopes
We introduce a formal theory of syntax with scoped operations. Examples of such operations include "catch" for handling exceptions or delimiters for nondeterminism (like "once" known from Prolog). Scoped operations are known not to be algebraic in the sense of Plotkin and Power, hence syntax with scoped operations cannot be modelled by terms (or free monads) over signatures.
We introduce two models, one generalises Ghani et al.'s monad of explicit substitutions, while the other is based on indexed sets is the style of Fiore et al.'s presheaf formalisation of syntax with variable binders.
Joint work with Tom Schrijvers, Nicolas Wu, and Mauro Jaskelioff