F#: See the F# website.

Language Design: Value Recursion and Mutually Dependent Objects, University of Tuebingen, November 2004.

Generics: Design and Implementation of Generics for the .NET Common Language Runtime. PLDI, June 2001. See also a version given at Martin Odersky's group at EPFL later that year. Combining Generics, Pre-compilation and Application Domains. Extended version of a talk given at SPACE, Jan 2004. More light-hearted talk was a talk I gave at an MSR Press Day in 2004, entitled Catching the Tech Transfer Express.

Abstract IL: Two presentations on Abstract IL are Abstract IL, A Program Analysis and Manipulation Toolkit for .NET (Internal Microsoft Event, 2003) and An abstract model of MS-IL (A revised version of a talk from 2001) .

General .NET presentations: Innovations in Compilation in the .NET Platform, .NET Academic Days, Spain & Portugal, 2004. For those interested in history, here is an older overview of some of the work our lab has done in the context of .NET: Some .NET Research at MSR Cambridge. University of Cambridge Computer Laboratory, February 2001.

Leveraging .NET Meta-programming Components from F#: Integrated Queries and Interoperable Heterogeneous Execution, to be published at the ML Workshop, 2006, Portland, Oregon. Also in postscript.

Abstract. Language-integrated meta-programming and extensible compilation have been recurring themes of programming languages since the invention of LISP. A recent real-world application of these techniques is the use of small meta-programs to specify database queries, as used in the Microsoft LINQ extensions for .NET. It is important that .NET languages such as F# are able to leverage the functionality provided by LINQ and related components for heterogeneous execution, both for pragmatic reasons and as a first step toward applying more disciplined, formal approaches to these problems. This paper explores the use of a modest metaprogramming extension to F# to access and leverage the functionality of LINQ and other components. We do this by demonstrating an implementation of language integrated SQL queries using the LINQ/SQLMetal libraries. We also sketch two other applications: the execution of data-parallel quoted F# programs on a GPU via the Accelerator libraries, and dynamic native-code compilation via LINQ.

Initializing Mutually Referential Abstract Objects, published at the ML Workshop, 2005. See also the tech report MSR Tech Report 2005-31.

Abstract. Mutual dependencies between objects arise frequently in programs, and programmers must typically resort to manually filling 'initialization holes' to help construct the corresponding object graphs, i.e. null values and/or explicitly mutable locations. This report describes a 'base-line' proposal for a generalized form of value recursion in an ML-like language called initialization graphs, where value recursion is given the simplistic semantics of a graph of lazy computations whose nodes are sequentially forced, with uses of recursive values checked for initialization-soundness at runtime. We then develop examples using this mechanism to show how problematic the issue of value recursion is for ML-like languages, and in particular how sophisticated reactive objects cannot be defined in the language without using initialization holes, and how this forces ML programmers to break abstraction boundaries. At the same time we show how OO languages rely extensively on null pointers during initialization. We propose that a general, semi-safe mechanism allows value recursion to be used in conjunction with existing sophisicated abstract APIs such GUI libraries, and allows freshly defined APIs to be both abstract and yet not require clients to use explicit initialization holes. We propose that the initialization mechanism permits more programs to be expressed in the mutation-free fragment of ML, though we do not formally prove this result.

Pre-compilation for .NET Generics, Don Syme and Andrew Kennedy. Unpublished note, to be published as an MSR Tech Report.

Abstract. The Microsoft .NET Common Language Runtime (CLR) supports pre-compilation in order to help avoid the slow application start-up times and unnecessarily high memory usage often associated with virtual machine (VM) execution, However, Version 2 of the .NET Common IL (CIL) also supports generics, i.e. type parameters for data and code, in part implemented using template-expansion techniques, and the use of dynamic compilation for generics would threaten the gains of pre-compilation. We describes techniques to support the pre-compilation of generic CIL code, resulting in the first language implementations to support the combination of dynamic loading, pre-compilation and typeparameterization over unboxed representations. We discuss the load-time techniques used to resolve potential duplication and optimizations based on "preferred pre-compilation modules". We give performance results relating to code-size, code-duplication and start-up times as observed in our implementation of the techniques, aspects of which have been shipped in recent releases of v2.0 the Microsoft .NET CLR.

Formalization of Generics for the .NET Common Language Runtime With Andrew Kennedy and Dachuan Yu. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).

We present a formalization of the implementation of generics in the .NET Common Language Runtime (CLR), focusing on two novel aspects of the implementation: mixed specialization and sharing, and efficient support for run-time types. Some crucial constructs used in the implementation are dictionaries and run-time type representations. We formalize these aspects type-theoretically in a way that corresponds in spirit to the implementation techniques used in practice. Both the techniques and the formalization also help us understand the range of possible implementation techniques for other languages, e.g., ML, especially when additional source language constructs such as run-time types are supported. A useful by-product of this study is a type system for a subset of the polymorphic IL proposed for the .NET CLR.

An Industrially Effective Environment for Hardware Verification. With Carl Seger, Robert Jones, John O'Leary, Tom Melham, Mark Aagaard and Clark Barrett. In Submitted to IEEE Transactions on Computer-Aided Design of Integrated Circuits.

We describe the Forte verification environment for datpath-dominant hardware, which has proved effective in large-scale industrial trials. Forte combines an efficient linear-time logic model checking algorithm and symbolic trajectory evaluation with lightweight theorem proving in higher-order logic.

Combining Generics, Precompilation and Sharing Between Software-Based Processes. With Andrew Kennedy. In 2nd workshop on Semantics, Program Analysis and Computing Environments for Memory Management (SPACE), January 2004, Venice, Italy.

We describe problems that have arisen when combining the proposed design for generics for the Microsoft .NET Common Language Runtime (CLR) with two resource-related features supported by the Microsoft CLR implementation: application domains and pre-compilation. Application domain s are "software based processes" and the interaction between application domains and generics stems from the fact that code and descriptors are generated on a per-generic-instantiation basis, and thus instantiations consume resources which are preferably both shareable and recoverable. Pre-compilation runs at install-time to reduce startup overheads. This interacts with application domain unloading: compilation units may contain shareable generated instantiations. The paper describes these interactions and the different approaches that can be used to avoid or ameliorate the problems.

"So few publications? What on earth were you doing?"... 2002 and 2003 were devoted almost exclusively to being involved in the design and implementation of the support for generics in the .NET CLR. In particular, Andrew Kennedy and myself were largely responsible for the implementation of the support for generics in the core JIT, Execution Engine and pre-compilation components of the Microsoft .NET CLR implementation, as used by Microsoft's C# and Visual Studio products. We were also responsible for prototyping support in other areas.

Automating Type Soundness Proofs via Decision Procedures and Guided Reductions (PDF preprint, missing diagram). (Abstract). With Andy Gordon. Submitted to LPAR 02 in Tiblisi, Georgia, October 2002.  (Note, postscript with diagram, but which does not seem to display correctly in Ghostview is here, i.e. needs to be printed). 

ILX: Extending the .NET Common IL for Functional Language Interoperability. Published at Babel 01 in September 2001, Florence, Italy.

This paper describes several extensions to the .NET Common Intermediary Language (CIL), each of which is designed to enable easier implementation of typed high-level programming languages on the .NET platform, and to promote closer integration and interoperability between these languages. In particular we aim for easier interoperability between components whose interfaces are expressed using function types, discriminated unions and parametric polymorphism, regardless of the languages in which these components are implemented. We show that it is possible to add these constructs to an existing, ``real world'' intermediary language and that this allows corresponding subsets of constructs to be compiled uniformly, which in turn will allow programmers to use these constructs seamlessly between different languages. In this paper we discuss the motivations for our extensions, which are together called Extended IL (ILX), and describe them via examples. In this setting, many of the traditional responsibilities of the backend of a compiler must be moved to ILX and the execution environment, in particular those related to representation choices and low-level optimizations. We have modified a Haskell compiler to generate this language, and have implemented an assembler that translates the extensions to regular or polymorphic CIL code.

Design and Implementation of Generics for the .NET Common Language Runtime , (postscript, pdf) With A. Kennedy. Published at PLDI 2001 in June 2001, Snowbird Utah. Presentation (ppt).

The Microsoft .NET Common Language Runtime provides a shared type system, intermediate language and dynamic execution environment for the implementation and inter-operation of multiple source languages. In this paper we extend it with direct support for parametric polymorphism (also known as generics), describing the design through examples written in an extended version of the C# programming language, and explaining aspects of implementation by reference to a prototype extension to the runtime. Our design is very expressive, supporting parameterized types, polymorphic static, instance and virtual methods, "F-bounded" type parameters, instantiation at pointer and value types, polymorphic recursion, and exact run-time types. The implementation takes advantage of the dynamic nature of the runtime, performing just-in-time type specialization, representation-based code sharing and novel techniques for efficient creation and use of run-time types. Early performance results are encouraging and suggest that programmers will not need to pay an overhead for using generics, achieving performance almost matching hand-specialized code.

Typing a multilanguage intermediate code (abstract, postscript, pdf) With A. Gordon. In Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, pages 248-260, 2001.  An extended version of this paper appears as Technical Report MSR-TR-2000-106 (postscript, pdf), Microsoft Research, December 2000.

Three Tactic Theorem Proving, published at TPHOLs 99, in compressed postscript or postscript or pdf

An unpublished draft paper about the interface to DECLARE which needs some further work. Peruse it as compressed postscript or postscript or pdf.

My thesis as accepted by the University of Cambridge for a PhD, entitled ``Declarative Theorem Proving for Operational Semantics'' is available in your choice of postscript or compressed postscript or pdf.

Proving JavaS Type Soundness, University of Cambridge Computer Laboratory Technical Report 427, postscript or pdf

DECLARE: A Prototype Declarative Proof System for Higher Order Logic, (postscript, pdf) University of Cambridge Computer Laboratory Technical Report 416. You can read the abstract first if you fancy.

A New Interface for HOL - Ideas, Issues and Implementation (postscript, pdf) 1995 Conference on Higher Order Logic Theorem Proving and its Applications, Aspen Grove, Utah.

A Theory of Finite Maps, (compressed postscript). Co-authored by Graham Collins, then at the University of Glasgow. 1995 Conference on Higher Order Logic Theorem Proving and its Applications, Aspen Grove, Utah.

Reasoning about the Formal Definition of Standard ML using HOL, 1993 Conference on Higher Order Logic Theorem Proving and its Applications, Vancouver, Canada.

Mechanized Reasoning about Standard ML using HOL, (postscript, pdf) 1992 Australian National University Undergraduate Thesis.