William Blum's website

Research

Check out the publications pages to learn more about my research in formal computer science. Tools developed in relation with this research can be found here.


Game semantics

In my D.Phil thesis (2009) I introduced a novel presentation of Game Semantics based on a generalization of the theory of traversals. Traversals were originally introduced by Ong in the context of higher order recursion schemes. In my thesis, I extend the notion of traversals to the simply-typed lambda calculus and other extensions of it (e.g., PCF). I then introduce an alternative presentation of game semantics, called the revealed game semantics, where internal moves are preserved. Finally I formalize a correspondence between the game semantic denotation of a lambda term and its set of traversals.

The Correspondence Theorem \(\newcommand{\theroot}{\circledast} % the root of the computation tree \newcommand{\lsem}{[\![} % \llbracket \newcommand{\rsem}{]\!]} % \rrbracket \newcommand{\sem}[1]{{[\![#1]\!]}} \newcommand\travset{\mathcal{T}rav} \newcommand{\filter}{\upharpoonright} \newcommand{\syntrevsem}[1]{{\langle\!\langle #1 \rangle\!\rangle}_{\sf s}}\)

For every simply-typed term \(\Gamma \vdash M :T\), we can construct a bijection \(\varphi_M\) from the set of traversals over some abstract syntax representation of \(M\) and the revealed game semantic denotation of \(M\). Further, we can construct a bijection \(\psi_M\) from the set of traversals projected at the root \(\theroot\) of the abstract syntax tree of \(M\) and the standard game semantic denotation of \(M\): \[\begin{eqnarray*} \varphi_M &:& \travset(M : T)^\star \stackrel{\cong}{\longrightarrow} \syntrevsem{M} \\ \psi_M &:& \travset(M : T)\filter \theroot \stackrel{\cong}{\longrightarrow} \sem{M} \enspace . \end{eqnarray*}\]

The full technical details and proof this theorem can be found in Chapter 4 of my DPhil thesis. I have also extracted the relevant part in a technical report. I also gave an overview of the correspondence result and its proof at the Galop 2008 workshop.

Based on this result, I implemented a pedagogic tool for teaching Game semantics and the theory of traversals. The tool, written in F# and OCaml, can be downloaded here.

Higher-order recursion schemes

The study of the safety restriction led me to the study of higher-order recursion schemes. In an unpublished paper I showed that the type homogeneity constraint included as part of the original definition by Knapik et al. is in fact not necessary. The 12-page proof (pdf) consists in a game semantic argument based on the theory of traversals which is presented in details in my DPhil thesis.

The safe lambda calculus

The major part of my DPhil thesis concerns the study of a syntactic constraint for higher-order computations called the safety restiction. For the nitty gritty details I refer you to the online publication of my thesis.

Termination analysis of higher-order programs

Based on the work of Jones and Bohr, I propose an extension of the size-change principle introduced by Lee, Jones and Ben-Amram to a subset of ML featuring ground type values, higher-order type values and recursively defined functions. This constitutes the first attempt to adapt the size-change principle to a higher-order functional language ala ML featuring if-then-elsebranching and let rec definitions. I have implemented a tool based on the this work which is able to prove termination of non-trivial higher-order programs of both ground and higher-order types. This gives a termination decision tool for some subset of recursively defined function on natural numbers.

This is research was pursued as part of my Master in Computer Science (2004).