Affiliate Members

Becker, Moritz	Harris, Tim	Phillips, Andrew

Current Projects

The Programming Principles and Tools group develops techniques and models for understanding programs, programming abstractions and languages, and develops related technology to implement advanced techniques and tools for software development. Research areas for this group include automated testing and analysis of software for “bugs”; new programming languages to better harness the power of advanced computing including distributed systems and applications in specific areas such as systems biology; and developing more secure software through programming techniques as well as tools for analysing security.

• Abstract IL
  .NET Common IL is the binary format for .NET Common Language Runtime executables. There are many, many interesting applications for manipulating, analyzing and transforming .NET Framework executables, ranging from static analysis for error detection to transforming binaries to add dynamic security checks to building IL-IL optimization and profiling tools. More...
• Bisimulation and Refinement Reconciled
  This is a joint research endeavour between Oxford, Cambridge, Redmond, and Macau. It was motivated by its potential relevance to the design and development of a new model-checker, Zing, at Microsoft Research Redmond. It permits a combination of the benefits of two well-known methods of specifying and verifying correctness of distributed systems, one favoured at Oxford and the other at Cambridge. More...
  
• Access Control Based on Execution History
  Security is a major, frequent concern in extensible software systems such as Java Virtual Machines and the Common Language Runtime. These systems aim to enable simple, classic applets and also, for example, distributed applications, Web services, and programmable networks, with appropriate security expectations. More...

• Stack Inspection: Theory and Variants
  Stack inspection is a security mechanism implemented in runtimes such as the JVM and the CLR to accommodate components with diverse levels of trust. Although stack inspection enables the fine-grained expression of access control policies, it has rather a complex and subtle semantics. More...
• Cryptyc: Types for control patterns not just data structures
  Type systems for data structures in programming language have been getting better and gaining wider currency in the past ten years: witness the use of types in the JVM and the CLR for security and to enable automatic memory management. More...
• Cw
  Cw is an extension of C# for distributed asynchronous concurrency and XML manipulation. See also Polyphonic C#. More...

• F#
  Mixed functional/imperative programming is a fantastic paradigm for many programming tasks. Languages such as OCaml and Standard ML provide excellent general purpose programming languages suited to medium-advanced programmers who want simple yet highly expressive tools that boost their productivity, primarily by reducing the error rate, increasing their productivity through type inference, and basically letting them focus on the difficult parts of their applications. More...

• Generics for C# and .NET CLR
  We have been designing and prototyping support for "generics" in C# and the .NET Common Language Runtime. Generics are also known as polymorphism, parameterized types, or templates. Generics are one of the main new features in C# 2.0 [Hejlsberg et al., The C# Programming Language, Addison-Wesley], and will be supported by multiple .NET languages and by the whole .NET infrastructure. More...
• Grand Challenges for Computing Research
  The chief purpose of the formulation and promulgation of a grand challenge is the advancement of science. A grand challenge represents a commitment by a significant scientific community to work together towards a common goal, agreed to be valuable and achievable within a predicted timescale. The challenge is formulated by the scientists themselves as a focus for the research that they wish to pursue in any case. More...

• ILX: Extending the .NET Common IL for Functional Language Interoperability
  ILX provides a way of encoding three features found in many ML-like programming languages into .NET IL. These are discriminated unions, first-class function values and generics. If you plan on implementating a functional language for .NET and wish to produce typed, verifiable IL then you may find the SDK suitable as a backend for your compiler. More...

• Kiwi: Synthesis of Circuits from Parallel Programs
  The Kiwi project provides a technique for compiling parallel programs in C# and other .NET languages into parallel circuits which execute quickly on hardware like field programmable gates arrays (FPGAs). Our aim is to allow software engineers to accelerate their computations on hardware without having to learn how to program in a conventional hardware description language like VHDL or Verilog. Instead, we ask the program to write a parallel model of their computation which is then transformed into an efficient parallel circuit. This project is part of a wider project that explores how to program future heterogeneous many-core systems. More...
• Languages for Systems Biology
  Systems Biology is the emerging interdisciplinary study of complex biological systems from the point of view of relationships and interactions between different components. Many of these interactions are based on digital information (e.g. DNA) and on sophisticated information processing. "A major challenge is to give the technologists a deep understanding of biology and vise versa. In addition, the technologists, computer scientists and biologists must share a common language. This requires new approaches to describing and teaching biology." [Institute for Systems Biology] We work on representing the structure and function of biological systems via formal languages, for description, simulation, analysis and (eventually) compilation. More...
• New dimensions for Excel
  The goal of the "New dimensions in Excel" project is to empower end-user programmers (that is, Excel users who are not professional programmers) to tackle more challenging applications. At the moment, larger and more complex spreadsheets often require the help of a professional programmer to write part of the application in Visual Basic. Our extensions would extend the "reach" of what can be done without leaving the familiar cells-and-formulae paradigm that has proved so successful in practice. More...

• Polyphonic C#
  Polyphonic C# extends the C# programming language with new asynchronous concurrency abstractions, based on the join calculus. The language presents a simple and powerful model of concurrency which is applicable both to multithreaded applications running on a single machine and to the orchestration of asynchronous, event-based applications communicating over a wide area network. More...
• Process Compensation
  The design and implementation of compensations for long-running transactions in XLANG and BPEL. Contact: Tony Hoare. More...
• Samoa: Formal Tools for Securing Web Services
  An XML web service is, to a first approximation, a wide-area RPC service in which requests and responses are encoded in XML as SOAP envelopes, and transported over HTTP. Applications exist on the internet (for programmatic access to search engines and retail), on intranets (for enterprise systems integration), and are emerging between intranets (for the e-science Grid and for e-business). Specifications (such as WS-Security, now at OASIS) and early toolkits (such as Microsofts WSE product) exist for securing web services by applying cryptographic transforms to SOAP envelopes. More...

• Semistructured Data: Query languages for semistructured data based on spatial logics
  The ambient logic (see Spatial Logics) is a modal logic that describes the structural and computational properties of distributed and mobile computation. The structural part of the ambient logic is, essentially, a logic of labeled trees, hence it turns out to be an ideal foundation for query languages for semistructured data, much in the same way as first order logic is a fitting foundation for relational query languages. More...
• Spatial Logics
  Spatial logics are specification logics for describing the behavior and spatial structure of concurrent systems. Logics for concurrent systems are certainly not new, but the intent to describe spatial properties, and in particular the spatial structure of distributed and mobile systems, seems to have arisen only recently. We came to it through previous works on Ambients and the Ambient Logic. More...
• The Glasgow Haskell Compiler
  Haskell is a computer programming language. In particular, it is a polymorphicly typed, lazy, purely functional language, quite different from most other programming languages. The language is named for Haskell Brooks Curry, whose work in mathematical logic serves as a foundation for functional languages. More...
• The SML.NET Compiler
  ML is a strongly typed functional (and imperative) programming language originally developed at the University of Edinburgh around twenty years ago: the original language embodying a polymophic type system. There are now two variants: Standard ML (also known as SML), which has a formal definition most recently revised in 1997, and O'Caml, developed at INRIA in Paris. More...

Former Projects

• A compositional language for describing financial contracts
  Financial or insurance contracts such as interest rate instruments, equity linked options, foreign exchange contracts, credit derivatives and so on can become very complex. When they do, answering questions such as Is this contract equivalent to that one?'', and What is the value of this contract to me today?'', become correspondingly difficult. Indeed, it can be hard even to pin down the precise meaning of the contract.

  Based on ideas from the theory of computer programming languages, we offer a new approach to the specification and automated processing of financial contracts. Our new language of contracts'' allows us to precisely specify arbitrarily complex contracts; to build easily-extensible libraries of contracts; to perform valuations of complex contracts in a simple, modular way; and to perform other back office functions in a similar way.

  So far as we know, this is a uniquely systematic approach to the description and manipulation of financial contracts. Published at the International Conference on Functional Programming 2000, this work now forms the basis for a startup company in Paris, Lexifi Technologies. It has also inspired collaborative work between Microsoft Denmark (Jesper Kiehn) and the University of Copenhagen (Fritz Henglein), who are broadening the idea to cover non-financial contracts.

  This is joint work with Jean-Marc Eber, who is now CEO of Lexifi.

• Ambients
  We develop a simple uniform model to capture the behavior of dynamic wide-area computation, from local security protocols to world-wide networking. We use this model, for example, to describe active agents travelling on an open network between protected locations, to describe mobile connected devices, and to specify security and confinement properties.
• Research Languages and the .NET Framework
  We have worked with a number of academic partners from around the world to help them compile their favorite research languages to the .NET Common Language Runtime and to integrate them within Visual Studio. The list of languages includes Mercury, Scheme, Component Pascal, Eiffel, Oz, Oberon and Haskell.

back to top