24 Nov 04
King’s College, London, UK
One quantifier for forall and exists and generic elements or … unknowns are data
Murdoch J. Gabbay. Slides of a talk given at the departmental colloquium on 24 November 2004.
10 Sep 04
Imperial College, London, UK
Murdoch J. Gabbay. Slides of a talk given in Imperial College, London, on 10 September 2004. Thanks to Stephen Muggleton.
25 Aug 04
PPDP, Verona, Italy
15 Jul 04
Turku, Finland
14 May 04
LIX, Paris, France
Murdoch J. Gabbay, . 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.
4 May 04
PPS, Paris, France
Nominal Terms, Existential Variables, and Mathematics
Murdoch J. Gabbay. Talk given at PPS on 4 May 2004.
11 Mar 04
Murdoch J. Gabbay . We discuss extensions of the Nominal Terms framework introduced in Nominal Unification. Lots of blue sky, but pretty.
27 Feb 04
LRI
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).
Feb 04
LIX, Paris, France
Murdoch J. Gabbay, . 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.
9 Dec 03
King’s College, London, UK
Restart as a Computational Rule
Murdoch J. Gabbay, . Talk given on 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. See also an extended abstract (pdf).
2 Jun 03
Cambridge Uni, UK
30 May 03
Lisbon Uni, Portugal
28 May 03
Lisbon Uni, Portugal
20 Mar 03
ENS Lyon, France
Murdoch J. Gabbay. 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. See also an abstract.
13 Mar 03
Manchester Uni, UK
FM for Higher-Order Abstract Syntax
Murdoch J. Gabbay. 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. See also an abstract.
2 Mar 03
Cambridge Uni, UK
Restriction, binding, and three presentations of the pi-calculus
Murdoch J. Gabbay. 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.
11 Dec 02
JAIST, Japan
2 Dec 02
Pisa Uni, Italy
11 Nov 02
Cambridge Uni, UK
Theory and Models of the pi-calculus using Fraenkel-Mostowski Generalised
Murdoch J. Gabbay. Talk given in Cambridge on 11/11/2002 at the local group’s “Semantics Lunch”.
24 Oct 02
MPI, Saarbrücken, Germany
FM Techniques for Syntax-with-Binding
Murdoch J. Gabbay. Talk given at the Max-Planck Institute, Saarbrücken, Germany 24/10/02.
11 Oct 02
Paris, France
FM Techniques for Syntax-with-Binding
Murdoch J. Gabbay. 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.
2 Oct 02
IBM Research, Haifa, Israel
FM Techniques for Syntax-with-Binding
Murdoch J. Gabbay. Talk given at IBM Research, Haifa, Israel 2/10/02. Thanks to Cindy Eisner.
Apr 02
Heriot-Watt Uni, UK
FM-HOL. Contributed talk at Workshop on Thirty Five years of Automath, Informal Proceedings, Heriot-Watt University, Edinburgh, Scotland, April 2002.