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.

The literature on runtime “verification” (the activity of monitoring a running process to ensure compliance with a given specification) offers many different definitions of “monitorability” for properties. In a linear-time temporal setting, properties take the form of sets of behaviours (infinite sequences of states). In this talk, I will arrange the various monitorability classes found in the literature into a hierarchy along with well-known classes of properties such as safety and guarantee properties. I then give each of these monitorability classes neat topological characterisations within the topology induced by the "guarantee kernel" interior operator. Lastly, I show that the metric space used by Alpern and Schneider coincides with our topology.

We define a proper inductive semantics for LTL which includes those finite partial traces for which a definitive answer can be given: the “definitive prefixes” of the property. Sets of definitive prefixes are called definitive sets. Defining a semantics for LTL in terms of definitive sets gives us something equivalent to LTL3, a formulation popular in runtime verification. Our theory of definitive sets is sufficient to give a neat characterisation of (co-)safety and (co-)liveness properties, allowing us to straightforwardly prove Alpern and Schneider’s result that every property is the intersection of a safety and liveness property by simpler means.

In this talk I demonstrated how the well known Zipper structure of Huet, later generalised by McBride, can be used to equip any modal logic with inverse modalities. In particular, this allows us to equip any temporal logic, including CTL, with a notion of linear past.

In this talk I give whirlwind tour of denotational semantics, an oft-neglected but very important branch of theoretical computer science, which truly connects computer programs to mathematics

It’s well known that some problems in computer science are unsolvable — finding a recipe to tell whether an arbitrary computer program halts is a classic example. But in the world of concurrency, the most classical problem, mutual exclusion, is widely considered to be solved. In this talk we will examine the assumptions that have led concurrency theorists to this conclusion, and show that, unless either an assumption about hardware or a requirement of the problem are relaxed, this most famous problem of concurrency theory has, in fact, no satisfactory solution.

Most materials aimed at teaching people how to write, even within an academic context, focus largely on giving a rules-based framework for structure and prose style. These frameworks are based on outdated and inaccurate models of knowledge and are not suitable for academic writing. In this talk I will try to challenge some of the assumptions you have about writing papers, what (and who) writing papers is for, and how to think about writing as part of a research process.