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.


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).