Substitution and binders: a story of pseudo-monads
John Power – 25 May 2022
A little over 20 years ago, there were two concerted attempts to use sophisticated category theory to model binding in programming languages. One, by Gabbay and Pitts, uses the Schanuel topos and is particularly well suited to Milner's pi-calculus. The other, by Fiore, Plotkin and Turi, initially models substitution, that forming the technical heart of their work, with their modelling of binders flowing from it. Unbeknown to them at the time, pseudo-monads are central to their work, which is particularly well suited to the lambda calculus; and the setting of pseudo-monads allows their work to be extended routinely to several valuable variants of the lambda calculus. I wrote a string of papers about the situation with Miki Tanaka over a period of several years. I propose to outline the key ideas: the mathematics is simple for AusCat but the application to programming might be new and of interest to you.
Back