This year’s Oregon Programming Languages Summer School, organized by Bob Harper, Greg Morrisett and Zena Ariola, has come to a close after two amazing weeks. I wanted to take a moment to thank everyone who made my time here so pleasant, with special regards to Bob Harper and Mark Bickford, who patiently answered my numerous questions about Nuprl and Brouwerian mathematics.
something’s in the air: the nuprl zeitgeist
A good friend told me that he felt something in the air this past year, a sort of Nuprl Zeitgeist as it were; I must admit that I have felt the same thing, and it is truly bracing! After decades of undeserved obscurity, I have been hearing more whispers than ever about Nuprl and its computational type theory, and the verificationist meaning explanation seems to be moving toward a more appropriately central place in the public consciousness.1 I think it is inevitable that these whispers should turn into a shout.
It is fitting, then, that for this year’s OPLSS, the PRL group surprised everyone by making available virtual machines for using Nuprl locally. Now, the best Nuprl experience is still to be had by connecting to the central Nuprl cloud, but at the present time, the availability of virtual machines exposes many people to Nuprl who would otherwise simply not bother.
I have also been delighted with the response so far to JonPRL, which is my implementation of a Nuprl-like proof refinement logic for Computational Type Theory. My thanks to Bob Harper, Mark Bickford and Peter Dybjer for their patient guidance as I develop this project, and special thanks to Danny Gratzer for taking the time this week to learn how it works and implement many crucial features, including Doug Howe’s Computational Equivalence.2
The theme of OPLSS is “Computational Trinitarianism”, as coined by Bob Harper, but I and other students detected a distinct & invigorating undercurrent of meaning semantics and realizability, as alluded to in Harper’s lectures, and more fully developed in Dybjer’s and Constable’s.
Perhaps the most detailed exposition of the standard meaning explanation for type theory (albeit not dependent type theory) was contained in Amal Ahmed’s class on logical relations, where she developed the PER semantics, which is related in a very deep way to the two most prevalent interpretations of intuitionistic logic: realizability semantics (by way of interpreting the types as PERs of closed, canonical realizers) and Beth/Kripke semantics (with the generalization to the step-indexed logical relations).
Highlights of OPLSS for me were Bob Constable’s outstanding lectures, the hours that Mark Bickford spent teaching me about Nuprl, computational equivalence, intuitionistic mathematics, bar induction, and free choice sequences, and of course meeting Bob Harper, whose personality and sharply honed sense of scientific aesthetics is a constant inspiration to me.
Until next year!
With regard to the re-popularization of meaning semantics for type theory, I have tried to do my part by writing a self-contained introduction to them, entitled Type Theory and its Meaning Explanations.↩
Douglas J. Howe, 1989. Equality in Lazy Computation Systems. In this short paper, which is possibly one of the most influential in its area, Howe propounds a particularly well-behaved computational bisimulation relation which holds of any computation system that satisfies certain requirements. In one stroke, the numerous and complicated “direct computation” rules of Nuprl were replaced with a single principle, enabling equational reasoning for untyped open terms.↩