Which is worse? Ignorance or apathy? Who knows? Who cares?
Murdoch James Gabbay
Personal details
- Name
-
Everybody calls me Jamie.
Research and (academic) publications
I study the foundations of computer science. I’m known for inventing nominal techniques and nominal sets based on the Gabbay-Pitts model of naming and abstraction in Fraenkel-Mostowski set theory, for which Andrew and I received the 2019 Alonzo Church Award for Outstanding Contributions to Logic and Computation.
This work was initially with Andrew Pitts; then Mark Shinwell, Christian Urban, and James Cheney joined in.
DBLP says I’ve published with twenty-nine coauthors, including Maribel Fernández, Ian Mackie, Michel Reniers, Mohammed Reza Mousavi, Aad Mathijssen, Martin Hofmann, Stéphane Lengrand, Gilles Dowek, Michael Gabbay, Dominic Mulligan, Vincenzo Ciancia, Daniela Petrişan, Tadeusz Litak, Elliot Fairweather, Matteo Cimini, Claus-Peter Wirth, Dan Ghica, Aleksandar Nanevski, and Peter Kropholler.
You’re welcome to see the list of my publications on this website or Murdoch J. Gabbay on DBLP. For other curated sources see Murdoch J. Gabbay on Scopus and Murdoch J. Gabbay on Orcid.
Other publication-related items:
-
Since 2018 I’ve become interested in blockchains, and also the economic theory of Karl Marx (as applied to blockchains). More details on my publications list.
-
I’ve been published in the Times Higher Education. Here is a permalink to the article on how "The false market in degrees is ruining higher education". Many thanks to an excellent editor.
-
Finally, see some tips on writing papers and managing co-authors.
Software development
Coding is hard, but the same discipline that makes theorems elegant and papers beautiful, or courses clear and lectures engaging, can help make datastructures clean and code precise. You need to learn what’s idiomatic and efficient for a given language, and learn the tooling — and this takes time! — but that’s just matter of apprenticing yourself to someone familiar with a language and being humble and listening. I’ve been fortunate to have some excellent teachers.
The code below is open-source and available on my GitHub page. I hope you like it and may find it useful:
Nominal Datatypes package for Haskell
I am pleased to announce my Nominal Datatypes package for Haskell. This includes reference implementations of the untyped lambda-calculus, System F, and an EUTxO blockchain.
At time of writing, the GitHub version uses GHC8.10, which depends on a toolstack which creates warning messages about invalid magic. Sorry about this: it’s not GHC’s fault, and it’s annoying, but harmless.
I delivered a course based on the package in the Scottish Programming Languages and Verification Summer School (SPLV) in August 2020. Speakers were myself, Maribel Fernandez (Nominal rewriting and unification), Michel Steuwer (compiler intermediate representations), and Edwin Brady (the implementation of Idris 2).
Lecture recordings for the summer school are at this YouTube channel. Direct links for my course’s recordings are here: - Lecture 1 - Lecture 2 - Lecture 3.
See also my written course notes, being a mildly scrubbed transcription of the live coding during the lectures.
Cairo / Python development and testing
The Cairo abstract machine is an Ethereum Layer 2 virtual hardware based on polynomials over finite fields and written in Python. The motivation for Cairo is: execute off-chain then verify on-chain. This increases the blockchain’s effective on-chain processing power, because verification is cheaper than the initial execution.
I am pleased to announce:
-
The Cairo integer types library and
-
the Cairo test suite based on PyTest and Hypothesis (also on pip; and see this video presentation of the test suite).
The integer types library brings bitwise integer emulations to Cairo, which is needed because its native numerical type is the field element.
The test library helps me to test the integer types library, and more generally it introduces honest-to-goodness property-based testing to the Cairo ecosystem.
Citing me
If you use my work, I suggest you cite me as ‘Murdoch J. Gabbay’ rather than just ‘M. J. Gabbay’ because my brother Mike has the same initials.
The Gabbay-Pitts NEW quantifier
That’s the И symbol you’ll find in most of my papers: a quantifier meaning ‘for a fresh name’, with good logical properties. See my PhD thesis and subsequent LICS'99 paper. Here is LaTeX code for typesetting the NEW quantifier.
Talks
I have given academic talks on mathematics and theoretical computer science in universities and research institutes all over the world. Travelling and giving talks is a great way to improve and grow as an academic. Thanks to all those who kindly hosted me.
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.
Editorial work
-
I am happy to announce the Journal of Financial Technology, a free and open-access academic journal founded to provide a high quality venue to publish, promote, publicise, and develop the fusion of mathematics, statistics, computer science, finance, and law in the new field of fintech.
-
Handling editor and deputy editor-in-chief of the Journal of Logic of Computation.
-
Editor on the Journal of Applied Logics.
-
I have served as a referee for numerous conferences and journals. If I were smarter, perhaps I would have made a list. Be reassured though … I was very nice when I reviewed your submission.
Swedish Chef
For your convenience, my homepage is available in Swedish Chef (see Wikipedia and YouTube).
Scripts$
Sometimes I remember that computers are supposed to save labour as well as create employment for mathematicians. Then I write a computer script.
Photos
I was once a keen photographer. I took urban and scenic photographs of people, landscapes, animals, insects, architecture — and anything else that reflects or generates light. When I travelled, I usually had my camera with me.
I maintain two catalogues of photos:
-
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.
-
After that I got myself a Nikon DSLR. Take a look through my viewfinder.
I haven’t updated my online photo galleries in some time … I hope to do this when I get an opportunity.
Classification codes
I am not a number — but if I were:
Keywords
of some things I have worked on, in no particular order.
-
(Stone) duality and representation theory.
-
Nominal rewriting and unification.
-
Nominal algebra.
-
Fraenkel-mostowski set theory and models.
-
The NEW quantifier (LaTeX code here).
-
Nominal logic, first-order logic, higher-order logic.
-
The NEW calculus of contexts and the lambda context calculus.
-
Restart.
-
a-logic.
Further reading
-
Foundations of nominal techniques and Nominal terms, nominal logics, two papers summarising the technical content above.
-
Two-level nominal sets provides the most technically sophisticated account so far of the "holes" X above (though I would say that, I suppose).
-
A recent paper which gives a nominal sets representation theorem for the NEW-quantifier; and another which gives a nominal sets representation theorem for name-generation. Further papers are here.
-
The Nominal Methods Group, who are working on implementing nominal techniques in Isabelle.
Tasting notes
I like alcohol, especially strong beers and malt whisky.
I keep some tasting notes online.
Jewish festivals
Perform a mitzva (a good deed); avoid scheduling events on Shabbat, Rosh Hashanah, Yom Kippur, Sukkot, Chanukkah, Purim, and Passover.
- Introduction to Jewish holidays
-
Minimal information about 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.
(Links from Philip Wadler’s homepage.)
Essays and opinions
I keep a miscellanea of opinions.
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.
Jekyll
These pages were coded using Jekyll.
Fonts
Fonts used on this webpage are:
-
Roboto Slab by Christian Robertson. At the time of writing he is the lead visual designer for Android (so if you use an Android phone, you’re using his vision).
-
Inconsolata by Raph Levien, who has also worked on Gnome, Gimp, Gtk+, Ghostscript (a precursor to pdf), and other stuff that starts with G.