Person. Lawrence Paulson [lawrencepaulson]

Emeritus Professor of Computational Logic; Fellow at Clare College
University of Cambridge
https://www.cl.cam.ac.uk/~lp15/

Backlinks

Weeknotes 2025-W37 › College updates [01GW]

September 12, 2025
Jon Sterling

I finally managed to get an interviewing team put together for the coming Admissions season. This is one of many things that I have to deal with each year, and I am very grateful for my dear colleague Larry Paulson’s help and guidance as I get up to speed. Earlier this week, I wrote:

We don’t lecture that much at Cambridge, but this can create a bit of an illusion… We handle so many things amongst ourselves that other universities either don’t do at all or have administrative support staff for.

This is a good thing, because it impedes the bureaucratic takeover that has gutted the soul out of many other institutions, but it also means that either you quickly find a way to identify with the major tasks of the University and the Colleges *outside* of pure research, or you become frustrated and overwhelmed.

I chose the former, and I am more happy for it. I love my research, but I also love looking after my undergraduates in College, teaching them, assisting them with their careers, recruiting the next batch, etc. This is all part of what makes Cambridge a place that I love.

Becoming a Tutor [01GV]

September 12, 2025
Jon Sterling

I’ve decided to join our Tutorial team this year. For those who don’t know, at Cambridge each student has both a Director of Studies (who looks after your intellectual well-being) and a Tutor, who provides assistance on pastoral matters. There were multiple reasons that I decided to take on this role now, but one of them is that I want to get as involved as possible into all the elements of University and College life that impact students. It is very easy here to isolate oneself from student reality in a variety of ways, and you have to actively combat that impulse if you don’t want to be completely out of touch with the tasks of the University and its Constituent Colleges.

I am looking forward to learning the ropes from our wonderful Tutorial team in the coming year.

Biennial silver audit [01GU]

September 12, 2025
Jon Sterling

I am Junior Inspector of Plate at Clare College, which is a role that I would not have believed existed prior to coming to Cambridge. We have a great deal of very old and valuable silver (and gold), most of left to the college during the past four centuries by various Fellows—including the 16-17th Century mad scientist William Butler. Every two years we must check that we actually still have all this stuff and know exactly where it is stored. The final two days of this week have been spent doing very little else but cataloguing and reorganising when needed. It has been a very interesting experience, but I can’t say I am not looking forward to being finished—last night I actually dreamt that I was still in the cellar scrambling to find where a given piece is recorded, worrying I had marked the wrong row in the catalogue, etc.

Weeknotes 2025-W15 › Project Pterodactyl: yes, I’m building a new proof assistant › Locales in dependent type theory? [01A2]

April 9, 2025
April 11, 2025
Jon Sterling

The goal of Pterodactyl is to explore the adaptation of locales from Isabelle to dependent type theory, as a lightweight but extremely expressive alternative to type classes. My colleague Larry Paulson has written some great blog posts about locales in Isabelle, and I strongly recommend reading Ballarin’s Exploring the Structure of an Algebra Text with Locales to get a feel for what is possible. Here is what locales do:

Locales appear to completely solve the pain involved when building up hierarchies of mathematical structures and notations, allowing you to effortlessly combine theories along a common core (e.g. defining rings in terms of a multiplicative monoid and an Abelian group sharing the same carrier).
Locales allow you to add new methods to a theory after the fact, and they will magically be available on anything that extended that theory. You can also add new links in the theory graph, and both cycles and diamonds are allowed so long as they are coherent; this is useful if you want to silently regard (e.g.) the space of endomaps on a set as a monoid, etc.

In comparison to modules and type classes, the strength of locales is that you don’t have to decide ahead of time whether you want to “bundle” fields with their carriers, etc. In contrast, a great deal of the difficult work of mathematical library design and maintainance in tools like Rocq, Agda, and Lean is figuring out just what things to bundle, and fixing things when your choices inevitably lead to breakage, etc. Locales avoid these problems entirely.

Finally, a reasonably usable locale implementation can be obtained without any higher-order unification whatsoever. I have a feeling that will be extremely important, given how unreliable (and incorrect!) most implementations of higher-order unification are; the situation is so bad that it is actually an open problem to define a correct higher-order unification algorithm in the presence of singleton types (such as the unit type). I do think that this can be solved (and may have already been solved by András Kovács), but my point is that the prognosis for unification in dependent type theory is bad.

Related

Institution. Clare College [00GP]

Constituent College
University of Cambridge
https://www.clare.cam.ac.uk/

Institution. University of Cambridge [ucam]

https://www.cam.ac.uk/