Talks (2005)

Murdoch J. Gabbay.  Talk given at the second CANS meeting in King’s College London, UK, on December 6. We present Nominal Algebraic Specifications, a theory of universal algebra based on Nominal Terms and thus able to algebraically specify, in a suitable sense, theories-with-binding. We show how an algebraic theory of first-order logic leads to “one-and-a-halfth-order logic”, which is above first-order logic and slightly to the side of second-order logic. We discuss proof-methods for the system and possible extensions. Thanks to Maribel Fernández.

Murdoch J. Gabbay.  Talk given at the University of Utrecht’s Institute for Logic, Language, and Computation, in their colloquium on mathematical logic on December 2. We present one-and-a-halfth-order logic, which is a logic somewhere above first-order logic and slightly to the side of second-order logic. It satisfies cut-elimination, has an algebraic presentation, and allows to quantify over all predicates in an interesting and unusual way. Thanks to Benedikt Loewe.

Murdoch J. Gabbay.  Talk given at the Foundations Group seminar of the Brouwer Institute in Radboud University in Nijmegen on November 29. We give a relatively technical sketch of FM techniques, Nominal Logic, and their application to reasoning on syntax-with-binding. Thanks to Henk Barendregt and Bas Spitters.
I gave the same talk at the Logic and Semantics Group’s Joint Theory semainar (‘Joint’ between Queen Mary and Westfield College and Imperial College) at Queen Mary and Westfield College on December 7. That time, it was under the name “Fraenkel-Mostowski Techniques: a NEW model of freshness and abstraction”. Thanks to Peter O’Hearn.

One member of the audience in Nijmegen then kindly invited me to give the talk again at the Theoretical Computer Science department in the Vrije Universiteit Amsterdam on December 12 (I used the original title). Thanks to Jan-Willem Klop and Femke van Raamsdonk.

Murdoch J. Gabbay.  Talk given in the Logic Tea series at the University of Amsterdam on November 22. We discuss a-logic, a first-order logic with a predicate atom which is true of variable symbols and false of non-variable symbol terms. We axiomatise the untyped lambda-calculus by way of example and discuss what models look like, some possible future work, and the design decisions (and some of the sins) hidden in the paper. Thanks to Johan van Benthem and Olivier Roy.

Murdoch J. Gabbay.  Talk given at London South Bank University on November 8 and at University College London on November 9. We discuss Nominal Algebraic Specifications, an algebraic framework tailored to axiomatising systems-with-binding such as the lambda-calculus and logic. Thanks to Jonathan Bowen and Robin Hirsch.

Murdoch J. Gabbay.  Bleeding-edge talk given in Eindhoven in a group workshop on 31 October 2005. We give a speculative account of an algebraic version of the NEW calculus of contexts.

Murdoch J. Gabbay.  Talk given at Tel-Aviv University on 6 October 2005. We give a non-technical account of Nominal Rewriting. Thanks to Arnon Avron and Nachum Dershowitz.

Murdoch J. Gabbay.  Talk given at Leicester University on 9 August 2005. We discuss Nominal Rewriting and suggest why it and the methods underlying it are of interest.

Murdoch J. Gabbay.  Talk given at LMU in Munich on 26 July 2005. We give a broad view of our research, mentioning a-logic and a whole load of other stuff.

Murdoch J. Gabbay.  Talk given at South Bank University in London on 25 July 2005. We discuss Restart, a Natural Deduction rule which turns intuitionistic logic into classical logic, without affecting proof-normalisation.

Murdoch J. Gabbay.  Talk given at PPDP’05 in Lisbon on 10 July 2005. We discuss a lambda-calculus with a hierarchy of variables of different ‘strengths’ (corresponding roughly to increasingly ‘meta’ variables). We find it to be remarkably expressive, and suggest that we can encode records, modules, objects, dynamic binding and rebinding, and many other constructs involving non-capture-avoiding substitution.

Murdoch J. Gabbay.  Talk given at PPDP’05 in Lisbon on 10 July 2005. We discuss two notions of binding which exist side-by-side in Extended Nominal Rewriting; one modelling lambda-calculus-like abstraction, the other modelling pi-calculus-like restriction. Some typos fixed with respect to the similar talk in Paris, and only 30 minutes long.

Murdoch J. Gabbay.  Talk given at LIX, Ecole Polytechnique, France, on 24 May. Thanks to Dale Miller. We discuss two notions of binding which exist side-by-side in Extended Nominal Rewriting; one modelling lambda-calculus-like abstraction, the other modelling pi-calculus-like restriction.

Murdoch J. Gabbay.  Talk given at the Binding Challenges workshop in JAIST, Ishikawa, Japan. Thanks to Rene Vestergaard. We speculate on an interesting way in which it may be possible to encode syntax-with-binding in a higher-order logic based theorem-proving environment.

Murdoch J. Gabbay.  Slides of a talk given at the CWI in Amsterdam on 2 March, and TUE in Eindhoven on 3 March. Thanks to Anton Wijs and MohammadReza Mousavi.

Murdoch J. Gabbay.  Slides of a talk given in INRIA Rocquencourt Paris, on 21 February, and PPS Paris, on 22 February. Thanks to James Leifer, Russ Harmer, and the people of PPS and INRIA.