gabbay:200512-kings-autfol
Murdoch J. Gabbay Automating first-order logic, 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 Fernandez.
[ps] [pdf]
gabbay:200512-utrecht-oneaah
Murdoch J. Gabbay One-and-a-halfth-order logic, 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.
[ps] [pdf]
gabbay:200511-radboud-noml
Murdoch J. Gabbay Nominal Logic and FM techniques: reasoning about binding without pain, 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.
[ps] [pdf]
gabbay:200511-amsterdam-alogic
Murdoch J. Gabbay a-logic, 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.
[ps] [pdf]
gabbay:200511-nomas
Murdoch J. Gabbay Nominal algebraic specifications, 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.
[ps] [pdf]
gabbay:200510-nomthv
Murdoch J. Gabbay Nominal terms with a hierarchy of variables, 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.
[ps] [pdf]
gabbay:200510-nomr
Murdoch J. Gabbay Nominal Rewriting. Or ... talking about functions, without functions, 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.
[ps] [pdf]
gabbay:200508-nomr
Murdoch J. Gabbay Nominal Rewriting, 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.
[ps] [pdf]
gabbay:200507-munich
Murdoch J. Gabbay a-logic, the lambda-calculus, and internalising meta using names and binding, 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.
[ps] [pdf]
gabbay:200507-resnr
Murdoch J. Gabbay Restart: a natural rule, 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.
[ps] [pdf]
gabbay:200507-newcc
Murdoch J. Gabbay A NEW calculus of contexts, 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.
[ps] [pdf]
gabbay:200507-extnrt
Murdoch J. Gabbay Extended Nominal Rewriting: two models of binding, 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.
[ps] [pdf]
gabbay:200505-extnrt
Murdoch J. Gabbay Extended Nominal Rewriting: two models of binding, 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.
[ps] [pdf]
gabbay:200504-istqwt
Murdoch J. Gabbay Is there a quick way to get names and binding in some nominal sense up and running in Isabelle/HOL polymorphically on the type-class ‘type’, without having to rewrite the whole thing from scratch — yes or no?, 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.
[ps] [pdf]
gabbay:200503-aspnr
Murdoch J. Gabbay Aspects of Nominal Rewriting, 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.
[ps] [pdf]
gabbay:200502-newcc
Murdoch J. Gabbay A NEW calculus of contexts, 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.
[ps] [pdf]