The Robert Harper Festschrift includes articles by three of Bob’s students and colleagues—Karl Crary, Andrzej Filinski, and Jonathan Sterling. Each of these articles touches on themes that are central to Bob’s research: module system design, proof-directed program development, and (to use Bob’s term) “computational trinitarianism”.

In this foreword to the Festschrift, we have additionally compiled reminiscences of Bob Harper from his PhD students. We invited them to reflect on their experiences working with and learning from Bob. We believe these reminiscences, presented in chronological order of dissertation date, deliver a most fitting tribute to Bob in honor of his 64th birthday.

Extending Martín Escardó’s effectful forcing technique, we give a new proof of a well-known result: Brouwer’s monotone bar theorem holds for any bar that can be realized by a functional of type (ℕ→ℕ)→ℕ in Gödel’s System T. Effectful forcing is an elementary alternative to standard sheaf-theoretic forcing arguments, using ideas from programming languages, including computational effects, monads, the algebra interpretation of call-by-name λ-calculus, and logical relations.

Our argument proceeds by interpreting System T programs as well-founded dialogue trees whose nodes branch on a query to an oracle of type ℕ→ℕ, lifted to higher type along a call-by-name translation. To connect this interpretation to the bar theorem, we then show that Brouwer’s famous “mental constructions” of barhood constitute an invariant form of these dialogue trees in which queries to the oracle are made maximally and in order.

We show how to systematically derive an efficient regular expression (regex) matcher using a variety of program transformation techniques, but very little specialized formal language and automata theory. Starting from the standard specification of the set-theoretic semantics of regular expressions, we proceed via a continuation-based backtracking matcher, to a classical, table-driven state machine. All steps of the development are supported by self-contained (and machine-verified) equational correctness proofs.

In ML-style module type theory, sealing often leads to situations in which type variables must leave scope, and this creates a need for signatures that avoid such variables. Unfortunately, in general, there is no best signature that avoids a variable, so modules do not always enjoy principal signatures. This observation is called the avoidance problem. In the past, the problem has been circumvented using a variety of devices for moving variables so they can remain in scope. These devices work, but have heretofore lacked a logical foundation. They have also lacked a presentation in which the dynamic semantics is given on the same phrases as the static semantics, which limits their applications. We can provide a best supersignature avoiding a variable by fiat, by adding an existential signature that is the least upper bound of its instances. This idea is old, but a workable metatheory has not previously been worked out. This work resolves the metatheoretic issues using ideas borrowed from focused logic. We show that the new theory results in a type discipline very similar to the aforementioned devices used in prior work. In passing, this gives a type-theoretic justification for the generative stamps used in the early days of the static semantics of ML modules. All the proofs are formalized in Coq.