Murdoch James Gabbay

Geometric church ceiling art

Welcome. I do research in mathematical computer science, specialising in the interface between logic, language, and semantics. I’m known for co-inventing the ‘nominal sets’ model of names and binding as variously implemented in nominal terms, nominal unification, nominal logic, nominal sets, nominal rewriting, nominal algebra—you get the idea. Names are hard-wired into the human brain and I try to understand them. Check out my publications online (with bibtex), or the nominal bibliography for a broad survey of papers in this area.
Simon Antoun, Andrew Dodd, and myself have designed an open source publications map program; see the a flash-based graphical map of my publications which I created using it.
I also take photographs.

Photograph of Murdoch J. Gabbay

Personal details

Name
Everybody calls me Jamie.
E-mail
murdoch.gabbay at gmail deletethis com


Summary

I work in theoretical mathematical computer science, studying foundational issues in the mathematics of programming—notably to do with names (referents) and compositionality.
I’m known for inventing nominal techniques and nominal sets, based on the Gabbay-Pitts model of naming and abstraction provided by Fraenkel-Mostowski set theory.
The work was initially with Andrew Pitts; then Mark Shinwell, Christian Urban, and James Cheney joined in. I have since published with Maribel Fernandez, Aad Mathijssen, Martin Hofmann, Stephane Lengrand, Gilles Dowek, Michael Gabbay, Dominic Mulligan, Vincenzo Ciancia, Daniela Petrişan, and Tadeusz Litak.
You can look at Murdoch J. Gabbay on DBLP (not always up-to-date!) or a full list of publications online with pdf links.
If you cite me, please cite me as ‘Murdoch J. Gabbay’ rather than just ‘M. J. Gabbay’ because my brother Mike has the same initials.

You may find a summary and motivation for my research interesting.
You may also find some LaTeX code to typeset the Gabbay-Pitts NEW quantifier useful. See also my full list of publications and academic talks.

Swedish Chef

For your convenience, my homepage is available in Swedish Chef (what’s that?).

Papers

I love writing maths papers; you can find my publications (with bibtex) here.

If linear lists aren’t your thing, there’s also the flash-based graphical map—the benefit being that links between papers, and the flow of development of the ideas, is immediately evident. You can make your own, using the publications map program.

Finally, see some tips on writing papers and managing co-authors.

Talks

I have given academic talks on mathematics and theoretical computer science in universities and research institutes all over the world.
Slides are online, and sometimes videos.

2012, 2011, 2010, 2009, 2008, 2007, 2006, 2005, pre-2005

Treatment of invited speaker

I travel a lot, and found this helpful guide to the treatment of invited speaker (sic) in the common-room of the Central Tungus Plateau University (Okrug campus), Siberia.

Essays and opinions

I keep a miscellanea of opinions.

Photos

I am a keen photographer.
I take urban and scenic photographs of people, landscapes, animals, insects, architecture — and anything else that reflects or generates light.
I travel, and I always have my camera with me.
Take a look through by viewfinder.

Until 2007 I used a Ricoh Caplio R4 — an exquisite little point-and-shoot, for its time. I learned a lot and a set of portraits, landscapes, macro shots, from my travels are online.

Classification codes

I am not a number — but if I were:

ACM Computing Classification System (1998)
F.4.1 Mathematical Logic
UNESCO subject classification codes (Spanish)
1102 Lógica deductiva

The Gabbay-Pitts NEW quantifier

A logic quantifier giving a mathematical meaning to ‘for a fresh name’.
It is based on the semantics for names and binding from my thesis and LICS’99 paper and forms the basis of nominal logic.
Here is LaTeX code for typesetting it.

Keywords …

… of some things I have worked on, in no particular order.

  • Nominal rewriting and unification.
  • Nominal algebra.
  • Fraenkel-mostowski set theory and models thereof.
  • The NEW quantifier (here you can cut-and-paste some LaTeX to typeset it).
  • Nominal logic, first-order logic, higher-order logic.
  • The NEW calculus of contexts and the lambda context calculus.
  • Restart.
  • a-logic.

Scripts$

Sometimes I remember that computers are supposed to save labour as well as create employment for mathematicians.
Then I write a computer script.

Academic activities

A summary of what I have published, where I have been, who I have worked with, and what journals and conferences I have been a referee or written a review for, then this (now out-of-date) list might help:
2006
2005

Tasting notes

I like alcohol, especially strong beers and malt whisky.
I keep some tasting notes online.

Jewish festivals

Be good, avoid scheduling events on Shabbat, Rosh Hasanah, Yom Kippur, Sukkot, Chanukkah, Purim, and Passover.

Introduction to Jewish holidays
Information about the traditions behind Jewish holidays (not a calendar).
Holiday dates for the next five years
A list, with dates in both the hebrew and western calendars, of the major holidays.
2011, 2012, 2013.
Dates (western calendar).
5771-5772, 5772-5773, 5773-5774
Dates (hebrew calendar).

(Links from Philip Wadler’s homepage.)

The Good, the Bad, and the Ugly

I keep a miscellanea of things I approve of, disapprove of, or am shocked by.

Hall of fame

I keep a hall of fame for programs which changed my life.

Brief summary and motivation for (a lot of) my research

Natural language has nouns and pronouns like “thing” and “it”, to denote things. This was used in the Middle Ages to designate a variable quantity, for instance in the equation “the thing plus two is three”. In the 16th century this was replaced by a letter, so the equation could be rephrased as x+2=3. To solve this equation is to find a number with which to replace x, thus, the significance of x is given by substitution.

In the 19th and 20th centuries x+2 was replaced by x → x+2 or λx.x+2 (read “x maps to x plus 2”). Though the variable may eventually be substituted, its primary purpose is to be bound by the symbol or λx. Perhaps surprisingly, this notion of binding can be used to specify and reason about notions of formal set theory (e.g. comprehension and replacement), logic (quantifiers), computation (lambda-abstraction), and linguistics (e.g. Montague grammars).

λ can be viewed as a term-former, constructing small structures out of larger structures, just as the ‘plus’ of addition + does. But what if we know the larger shape of what we want, but our knowledge of the internal parts is incomplete? (This is sometimes called bottom-up vs. top-down, or forward vs. backwards reasoning.) Then variables express not only substitution and binding, but also connectedness. For instance, the names a, b, c, and X are used below in all three senses:

(1)
λaλc.abc
 
(2)
(λaλc.X)[abc/X] =
λaλc.abc
 

Here λ is indicated by small black circles, and in diagram (1) names a and c are elided because they are bound. In diagram (2) the blue box X represents incompleteness into which we place abc. See how internal wires, which were anonymous in diagram (1), acquire names a and c in diagram (2) indicating how they should be connected.

Simple as these diagrams are, they underly a surprising amount of the mathematics broadly in use today. This is well-known by philosophers, logicians, computer scientists and linguists alike. What is lacking is a unified mathematics that accounts for names’ common features, and explains their indispensability to any form of logic, program or language. To put it simply but quite accurately: we need to understand the mathematics of structures like those represented above.

The recently-developed nominal sets, a mathematical semantics related to Zermelo-Fraenkel set theory and the pioneering foundational work of the early 20th century, provides a foundation for languages with the ability to handle names and based on a rigorous mathematical semantics; to synthesise theories of naming from formal logic, philosophy, and linguistics; and thus to outline a unified theory of names. This is a broad, but realistic programme: Zermelo-Fraenkel set theory, which can be thought of as the study of structures like diagram (1) above, has already been pivotal in unifying theoretical techniques from philosophy, mathematics, linguistics and computer science.

You might be interested in: