gabbay:200424-oneqfe
Murdoch J. Gabbay One quantifier for forall and exists and generic elements or ... unknowns are data, Slides of a talk given at the departmental colloquium on 24 November 2004.
[ps] [pdf]
gabbay:200409-nomu
Murdoch J. Gabbay Nominal Unification, Slides of a talk given in Imperial College, London, on 10 September 2004. Thanks to Stephen Muggleton.
[ps] [pdf]
gabbay:200408-nomr
Murdoch J. Gabbay Nominal Rewriting Systems, Slides of a talk at PPDP'04 on joint work with Maribel Fernandez and Ian Mackie, given in Verona, Italy, on 25 August 2004.
[ps] [pdf]
See also the paper.
gabbay:200407-seqcnl
Murdoch J. Gabbay A Sequent Calculus for Nominal Logic, Slides of a talk at LICS'04 on joint work with James Cheney, given in Turku, Finland, on 15 July 2004.
[ps] [pdf] See also the paper.
gabbay:200405-frelog
Murdoch J. Gabbay, Fresh Logic, We discuss Fresh Logic (joint work with James Cheney) and consider its relation to FOLN a logic by Miller and Tiu, especially in the light of insights from implementation. Talk given to the PARCIFAL group at LIX on 14 May 2004.
[ps] [pdf]
gabbay:200405-nomtev
Murdoch J. Gabbay, Nominal Terms, Existential Variables, and Mathematics Talk given at PPS on 4 May 2004.
[ps] [pdf]
gabbay:200403-extnt
Murdoch J. Gabbay, Extensions of Nominal Terms, We discuss extensions of the Nominal Terms framework introduced in Nominal Unification. Lots of blue sky, but pretty.
[ps] [pdf]
gabbay:200402-nomr
Murdoch J. Gabbay, Nominal Rewriting, We present Nominal Rewriting, an essentially first-order rewriting system with inbuilt support for alpha-equivalence. See also "Incomplete lambda-terms" below. Talk given in LRI in their seminar series (27/2/2004, 10:30am).
[ps] [pdf]
gabbay:200402-lamti
Murdoch J. Gabbay, Incomplete lambda-terms, We use Nominal Rewriting to specify and discuss a lambda-calculus with meta-variables and explicit substitution. Talk given in LIX as part of a series of informal talks on meta-variables.
[ps] [pdf]
gabbay:1203-restart-talk
Murdoch J. Gabbay, Restart as a Computational Rule, Talk givenon applying the Curry-Howard correspondence to a novel Restart Logic. Given in the Workshop on Lambda Calculus, Type Theory, and Natural Language in King's College London, on 9 December at 12:00 on work.
[extended abstract (pdf)] [ps] [pdf]
gabbay:0603-semantics-lunch
Murdoch J. Gabbay, Fresh Logic: Vanilla First-Order Logic with FM?, Talk given on Fresh Logic (a first-order logic for the NEW-quantifier with proof-normalisation) on 2 June at the local group's weekly Semantics Lunch.
[abstract] [ps] [pdf]
gabbay:0503-Lisbon-FreshML, gabbay:0503-Lisbon-pi
Murdoch J. Gabbay, FreshML: programming with binders made easy,
Murdoch J. Gabbay, FM binding for pi-calculus transitions,
Talks to be given on May 28 and 30 respectively at Fundacao da Faculdade de Ciencias e Tecnologia / University of Lisbon. Thanks in advance to Luis Caires and his department.
[abstract] [ps] [pdf]
[abstract] [ps] [pdf]
gabbay:0303-Lyon
Murdoch J. Gabbay, FM and the pi-calculus, I investigate what happens if we consider an FM-like category of objects with a finite name-for-name renaming action (possibly non-injective maps between names) rather than a finite name-for-name permutation action as is the case for FM sets. I obtain a category similar to Schan, but which supports a natural interpretation of weak HOAS. Talk given on March 20 at the ENS Lyon, France. Thanks to Daniel Hirschkoff.
[abstract] [ps] [pdf]
gabbay:0303-manchester
Murdoch J. Gabbay, FM for Higher-Order Abstract Syntax, I investigate what happens if we consider an FM-like category of objects with a finite name-for-name renaming action (possibly non-injective maps between names) rather than a finite name-for-name permutation action as is the case for FM sets. I obtain a category similar to Schan, but which supports a natural interpretation of weak HOAS. Talk given on March 13 in Manchester University, thanks to Peter Aczel.
[abstract] [ps] [pdf]
gabbay:feb-sem-lunch
Murdoch J. Gabbay, Restriction, binding, and three presentations of the pi-calculus, I've been using FreshML to program a pet interest of mine; transition systems and bisimulation checkers for the pi-calculus (see [gabbay:thempc]). I'll show excerpts from the programs I've written and talk about what writing them has taught me about another interest of mine; finding a semantics for restriction as distinct from binding. The sourcecode discussed is the pi-ltsb series of programs above, see [pi-ltsb] above.
[ps] [pdf]
gabbay:jaist-talk-0212
Murdoch J. Gabbay, FM for Names and Binding, Talk given on 11/12/2002 at the Japan Advanced Institute of Science and Technology, Ishikawa, on 14/12/2002 at MLG 2002 in Kinosaki, and on 16/12/2002 at ALGI in Kyoto. Thanks to René Vestergaard.
[ps] [pdf]
gabbay:200212-pisa
Murdoch J. Gabbay, Models of pi-calculus behaviour using FM techniques, Talk given in Pisa on 2/12/2002. Thanks to Ugo Montanari.
gabbay:thempc-talk
Murdoch J. Gabbay, Theory and Models of the pi-calculus using Fraenkel-Mostowski Generalised, Talk given in Cambridge on 11/11/2002 at the local group's “Semantics Lunch”.
[ps.gz]
gabbay:200210-mpi-talk
Murdoch J. Gabbay, FM Techniques for Syntax-with-Binding, Talk given at the Max-Planck Institute, Saarbrücken, Germany 24/10/02.
gabbay:200210-France-talk
Murdoch J. Gabbay, FM Techniques for Syntax-with-Binding, Talk given at INRIA Rocquencourt France 11/10/02 and Université Paris VII France 14/10/02. Thanks to Gilles Dowek and Pierre-Louis Curien.
[ps.gz]
gabbay:200210-IBM-talk
Murdoch J. Gabbay, FM Techniques for Syntax-with-Binding, Talk given at IBM Research, Haifa, Israel 2/10/02. Thanks to Cindy Eisner.
[ps.gz]
gabbay:fmhotn-talk
Murdoch J. Gabbay, FM-HOL, Contributed talk at Workshop on Thirty Five years of Automath, Informal Proceedings, Heriot-Watt University, Edinburgh, Scotland, April 2002.
[pdf, ps]