Abstract syntax and variable binding

By Marcelo P. Fiore, Gordon D. Plotkin, D. Turi. 1999

We develop a theory of abstract syntax with variable binding. To every binding signature we associate a category of models consisting of variable sets endowed with compatible algebra and substitution structures. The syntax generated by the signature is the initial model. This gives a notion of initial algebra semantics encompassing the traditional one; besides compositionality, it automatically verifies the semantic substitution lemma.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Citations in the corpus

A New Approach to Abstract Syntax with Variable Binding (2002, methodology): “These ingredients also occur in subsequent work on modelling -calculus names in SetI [FMS96, Sta96b] and, most relevantly, recent work on modelling variable-binding abstract syntax [ FPT99 , Hof99], where other presheaf categories besides SetI are considered.”
Initial Semantics for Strengthened Signatures (2012, background): “The signatures we consider here are much more general than the signatures in [7], and cover the signatures appearing in [16, 12].”
Monads need not be endofunctors (2010, background): “[7] described it as a monoid in a monoidal structure on [Fin,Set].”
Monadic Presentations of Lambda Terms Using Generalized Inductive Types (1999, background): “Turi [ FPT99 ] who pursue a more abstract algebraic treatment of signatures with binders but do not cover the simply typed case.”
Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures (2016, methodology): “The composition functors of these Kleisli bicategories can be understood as generalizations of various kinds of substitution monoidal structures [22, 23, 24, 25, 27, 36, 57], among those giving rise to the notions of a many-sorted Lawvere theory and of a coloured operad.”
Second-Order and Dependently-Sorted Abstract Syntax (2008, methodology): “Recall that the model of [11] is given by the functor category F = Set for F the category of finite sets (over a fixed countably infinite set of variables) and functions between them.”
Free-Algebra Models for the pi-Calculus (2005, background): “Similar categories of varying sets also appear in models for variable binding [5] and name binding (see, for example, [33] and citations there).”
Nominal Logic: A First Order Theory of Names and Binding (2001, background): “Hamana’s logic programming language [21] based on the presheaf semantics of binding in [ 11 ]).”