Erasure can destroy or hide information, sometimes in plain sight. This talk is about an experiment in compiling Lean to Plutus Core (Cardano's smart contract language) and back again, and its connection with Phil's paper "The Girard-Reynolds isomorphism".

The talk will give an overview of Phil's contributions to session types.

Classical Processes is a process calculus interpretation of Classical Linear Logic. Nominally, CP interprets CLL's axiom as a forwarder process, which sends any message it receives over its input channel over its output channel. Operationally, CP's forwarders do not forward messages at all. Instead, they put their input and output channels together and terminate. This causes lots of trouble with CP's metatheory and its use as a model of concurrent computation.

I propose an alternative operational semantics for forwarders which avoids this trouble and has a pleasant interpretation in CLL.

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.

In 2024, Philip Wadler proposed Explicit Weakening, a novel formulation of substitution in which many facts about substitution can be proved by reflexivity in a proof assistant such as Agda. The approach dispenses with renamings by making weakening explicit in the syntax.

We pick up where Wadler left off. We discuss the limitations of explicit weakening and propose an alternative that revives renamings while retaining its main advantage for mechanized proofs. Our approach uses rewriting type theory with a confluent selection of equations from the σ-calculus with first-class renamings. We validate the approach on substantial System F developments, including canonicity and logical-relations proofs.

Phil, Peter, and I have been exploring polymoprhic gradual typing since the COVID-19 pandemic. The improvements to Zoom removed the geographic barrier of our homes being in Edinburgh, Rio de Janeiro, Freiburg, and Bloomington. Our goal has been to develop a beautiful calculus that supports interoperability between dynamically typed regions of code and polymorphic, statically typed regions of code. We've explored many variations on the calculus, most of them based on a polymorphic variant of Fritz's Coercion Calculus. The latest version has a beautiful reduction semantics, but mechanizing the gradual guarantee is quite difficult. Even adding Codex and Claude to our collaboration has not yet yielded the proof! Nevertheless, we've learned a lot in the process, which I an happy to share in this talk.

The dactylic hexameter is a metrical system that governs the prosody of many pieces of ancient poetry, including the Homeric epics. In Ancient Greek, the assignment of a quantity (long or short) to a syllable can largely be "decided" by the language's writing system. This remarkable correspondence has been extensively studied by both linguists and classicists for centuries.

Nonetheless, a formally inclined person would find the current state of the art lacking: the correspondence is informally stated, ambiguous, and often idiosyncratic; no standardized rule set is agreed upon, and no computational method or artifact attempts to explicate it.

We do the matter justice by formally transcribing the relevant parts of Pharr's "Homeric Greek" textbook to Agda code. The process involves casting prosodic rules into typed inference rules, resolving potential conflicts, and managing ambiguities. By the end, we turn a previously informal "decision" into a decision procedure proper, proven sound and complete against our formalization. The result is an interactive artifact annotating >99.9% of the Iliad's verses with at least one prosodic proof-derivation, the first of its kind in providing explanations alongside metrical analysis.

I first met Philip Wadler exactly 30 years ago. Since then, our paths have crossed in several occasions, some times by chance and some times by design. In this completely untechnical talk, I will relate some of these interactions and the joy of being close to someone like Philip.