My DPhil research has mainly concerned Collapsible Pushdown Automata (CPDA). Whilst a standard pushdown automaton contains a stack of atomic values, a higher-order stack contains a stack of stack of stacks... adding additional structure in the form of `links' yields a collapsible pushdown stack. This somewhat technical definition yields an automaton capable of generating the same class of trees as Higher Recursion Schemes, systems of rewrite rules that show good promise as a model for higher-order functional programs. My DPhil research included seeking characterisations of the structures generated by such devices (which has led to the invention of the isophilic and dendrisophilic classes of structures) as well as addressing model-checking problems for them with respect to logics such as the mu-calculus, MSO and first-order logic. It was also concerned with understanding the expressive power of CPDA relative to the various constraints on recursion schemes, which has connections with Game Semantics.
I came to Oxford in 2003 for an undergraduate degree in Mathematics and Philosophy. From 2007 to 2011 I worked under the supervision of Prof. Luke Ong towards a DPhil and have now begun work as a PostDoc in LIAFA (CNRS and Université Diderot Paris-Paris 7), funded by La Fondation Sciences Mathématiques de Paris.
The Limits of Decidability for First Order Logic on CPDA Graphs
Christopher H. Broadbent
Recursion Schemes and Logical Reflection
Christopher H. Broadbent‚ Arnaud Carayol‚ C.−H. Luke Ong and Olivier Serre
In LICS. Pages 120−129. 2010.
On Global Model Checking Trees Generated by Higher−Order Recursion Schemes
Christopher H. Broadbent and C.−H. Luke Ong
In FOSSACS. Pages 107−121. 2009.