Person. Marcelo Fiore [marcelofiore]

Professor
University of Cambridge
0000-0001-8558-3492
https://www.cl.cam.ac.uk/~mpf23/

Backlinks

Wadler 70 [loc-005I]

September 10, 2026
Liam O'Connor

While his birthday was back in April, to fit with Plotkin 80 and LFCS 40, we had a birthday event for Philip Wadler today, celebrating his 70th year.

I really loved Conor's talk on dependent session types, which was inspired by a question from Phil ten years earlier at his 60th birthday event. Her proposed design resembles Peter Hancock's interaction structures quite a bit. Very nice work.

I also gave my talk, which I peppered with many anecdotes about meeting Phil. I got a lot of interest about potentially using Holbert-ng, including from Marcelo Fiore among others. Very exciting stuff!

Reference. Down with Linear Mathematical Developments [oconnor-2026-wadler70]

September 10, 2026
Liam O'Connor
Wadler 70 Meeting, University of Edinburgh, Scotland

This talk presents some of my recent rough work on educational proof assistants. I spent many years building Holbert — a graphical proof assistant and document preparation system — with the eventual goal of writing a PL textbook in it. But Holbert's design, like that of most proof assistants, forces exposition to follow a single linearisation of the dependency order of definitions and theorems, which is a poor fit for good mathematical writing. This talk demonstrates work in progress on the next generation of Holbert, built on top of Forester, the notes system by Jon Sterling and Kento Okura. Forester's transclusion mechanism lets self-contained notes on definitions and theorems be composed bottom-up into a document. Holbert-NG maintains its own separate graph of mathematical dependencies, independent of Forester's document graph, decoupling how a text is composed from the dependency structure of its mathematics.

Related

Institution. University of Cambridge [cam]

Cambridge, United Kingdom
https://www.cam.ac.uk/