A New Approach to Abstract Syntax with Variable Binding

By Murdoch James Gabbay, Andrew M. Pitts. Formal Aspects of Computing, 2002

644 citations recorded by the source corpus.

How researchers see this paper

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

A spatial logic for concurrency (part I) (2003, methodology): “Before defining safe substitution on processes, we first introduce transposition, and then define α-congruence in the style of [19].”
Free-Algebra Models for the pi-Calculus (2005, methodology): “In the equations for new we write x.p for the term p indexed by fresh x, borrowing Gabbay and Pitts’s notation for atom abstraction [ 9 ].”
Nominal Sets: Names and Symmetry in Computer Science (2013, background): “Exercise 2.1 gives an equivalent formulation of supp x from Gabbay and Pitts (2002).”
Nominal Logic: A First Order Theory of Names and Binding (2001, methodology): “The work described here draws upon joint work with Gabbay described in [10] [24] [11].”
A sequent calculus for nominal logic (2004, methodology): “10 in [4], the N-quantifier satisfies the “some/any” equivalences”
Second-Order and Dependently-Sorted Abstract Syntax (2008, background): “Such a development is well-known for first-order syntax, and it has more recently been extended to incorporate variable binding [11, 12].”
Nominal Techniques in Isabelle/HOL (2005, methodology): “Our work is based on the nominal logic work by Pitts e al [11,26].”