Many of my presentations are now online, and I have lso updated my publications page.

I joined Microsoft Research in 1998.  Before that I was a PhD. student at the University of Cambridge Computer Laboratory. Some time ago I spent three months at SRI and a six month jaunt at Intel. Clearly my ultimate aim is to work for everyone in the computing game, so I'll throw in links to IBM, Sun and Compaq for good measure.  Before all of this, I graduated from the Australian National University in 1993. 

Recently my research has revolved around Common IL and the Microsoft .NET Framework, and in particular the Microsoft .NET Common Language Runtime. I am involved in the following projects here in Cambridge:

• The design and implementation of support for Generics in C#, the CLR, Visual Basic and other languages. This feature is now in the process of being released as part of the Visual Studio 2005 (aka "Whidbey") family of products and specifications. For example you can download and use generics in Visual C# 2005 Express.
• The design and implementation of F#, a compiler for a .NET functional programming language akin to the core language of OCaml. This is the first functional programming language implementation where other languages can directly access the constructs defined in the functional language in an intuitive and straight-forward way, i.e. a language with bi-directional interoperability. The language demonstrates how mixed imperative/functional programming can be smoothly integrated into the .NET programming landscape, and is also a fantastically productive language to program in! You can read more about F# on my blog.
• A study of value recursion in safe and semi-safe programming languages. This work shows the relationship between mutually-dependent objects in OO programming and value recursion in functional programming languages, and illustrate the problems that arise in the context of GUI, automata and other variations on stateful reactive programming because of ML's restrictions on value recursion . It also describes a semi-safe extension to ML called 'initialization graphs' that gives some insight into these problems.
• The design and implementation of Abstract IL, a toolkit for manipulating .NET Common IL binaries.  This is implemented using OCaml and F#.
• The design and implementation of ILX, where I extended the .NET Framework's Common IL with constructs such as polymorphism, closures, function types and algebraic datatypes. This is used to implement some aspects of F#.
• Some of the people I work with here at MSR Cambridge include Andrew Kennedy, Byron Cook, Cedric Fournet, Luca Cardelli, Georges Gonthier, Andy Gordon, Nick Benton, Claudio Russo and Simon Peyton-Jones.

Here are some of the people and projects I have had the good luck to have been involved with:

• From 1999 to 2004 I worked extensively with the .NET Common Language Runtime Team, both on the design and implementation of generics and on other issues related to the .NET Common IL's type system. During 2002 and 2003 Andrew Kennedy and I were working essentially full-time as as an adjunct members of the CLR team in a mix of architectural, development, testing and program management roles (thankfully our workload has eased off...) Some of those who I had the pleasure of working with were Dario Russi, Vance Morrison, Sean Trowbridge, Simon Hall, Shri Borde, Ian Bearman, Chris Brumme and Patrick Dussud.
• From 1999 to 2003 I was involved with the design of C#, authoring the first draft of the C# language design for generics. I also prototyped the initial support for generics in the Microsoft C# compiler. During this time I had the pleasure of working with Anders Hejlsberg, Peter Golde, Peter Hallam and others.
• From 1999 to 2001 I was involved with the analysis of the verification rules for MS-IL, the intermediary language of the CLR, working with Andy Gordon and others.
• From 1999 to 2002 I was involved with Project 7, which brought together MSR, Microsoft and several academic groups to target languages at the .NET Common Language Runtime and to get these languages working together. Many aspects of the design of F# are the direct result of my involvement in Project 7.
• During my PhD I worked in with a range of people at the University of Cambridge Computer Laboratory, including Michael Norrish, Mark Staples , Tom Melham and Mike Gordon.
• In 1997 I greatly enjoyed working with the "Forte" team at Intel, including Carl Seger, Robert Jones, Mark Aagaard, Tom Melham and John O'Leary.
• In 1996 I worked with the PVS team including John Rushby and Natarajan Shankar.

My other research interests include the formal modelling of programming languages and abstract machines and techniques for the verification of their properties. Example machines include high level languages defined by operational semantics, stack machines such as the JVM, and hardware devices at various levels of abstraction. Typical properties include correctness (by correlating the machine against a higher-level specification) and type soundness (by proving the preservation of an appropriate invariant, which is implied by a statically checked condition). Typical techniques include model checking, automated reasoning, abstract interpretation and manual declarative proof.