π-calculus, Session Types research at Imperial College

Research Grants

Border Patrol: Improving Smart Device Security through Type-Aware Systems Design
Feb 2017 - Jan 2022
Turtles: Protocol-Based Foundations for Distributed Multiagent Systems
Nov 2016 - Oct 2021

Related grant: EP/N027965/1
Exploiting Parallelism through Type Transformations for Hybrid Manycore Systems
Oct 2013 - Sep 2018
From Data Types to Session Types - A Basis for Concurrency and Distribution
May 2013 - May 2019
Conversation-Based Governance for Distributed Systems by Multiparty Session Types
Jun 2013 - Jun 2018
Application Customisation: Enhancing Design Quality and Developer Productivity
Dec 2016 - Nov 2021
EU FP7 FET OpenX: UpScale
Feb 2014 - Jan 2017
COST Action IC1201 BETTY
Oct 2012 - Oct 2016

European Cooperation in Science and Technology, ICT Cost Action IC1201

Modern society is increasingly dependent on large-scale software systems that are distributed, collaborative and communication-centred. Correctness and reliability of such systems depend on compatibility between components and services that are newly developed or may already exist. The consequences of failure are severe, including security breaches and unavailability of essential services. Current software development technology is not well suited to producing these large-scale systems, because of the lack of high-level structuring abstractions for complex communication behaviour.

This Action will use behavioural type theory as the basis for new foundations, programming languages, and software development methods for communication-intensive distributed systems. Behavioural type theory encompasses concepts such as interfaces, communication protocols, contracts, and choreography. As a unifying structural principle it will transform the theory and practice of distributed software development.

The significance of behavioural types has been recognised world-wide during the last five years. European researchers are internationally leading. There is an urgent need for European co-ordination to avoid duplication of effort, facilitate interactions among research groups, and ensure that the field proceeds efficiently from academic research to industrial practice. This Action will provide the co-ordination layer and leverage the efforts of European researchers, to increase the competitiveness of the European software industry.
COST Action IC1405 Reversible computation
July 2015 -

European Cooperation in Science and Technology, ICT Cost Action IC1405 Reversible computation is an emerging paradigm that extends the standard forwards-only mode of computation with the ability to execute in reverse, so that computation can run backwards as naturally as it can go forwards. It aims to deliver novel computing devices and software, and to enhance traditional systems by equipping them with reversibility. The potential benefits include the design of revolutionary reversible logic gates and circuits - leading to low-power computing and innovative hardware for green ICT, and new conceptual frameworks, language abstractions and software tools for reliable and recovery oriented distributed systems.

Landauer’s Principle, a theoretical explanation why a significant proportion of electrical power consumed by current forwards-only computers is lost in the form of heat, and why making computation reversible is necessary and beneficial, has only been shown empirically in 2012. Hence now is the right time to launch a COST Action on reversible computation. The Action will establish the first European (and the world first) network of excellence to coordinate research on reversible computation. Many fundamental challenges cannot be solved currently by partitioned and uncoordinated research, so a collaborative effort of European expertise with an industrial participation, as proposed by this Action, is the most logical and efficient way to proceed.
COST Action IC1402 ARVI
April 2015 -

Runtime verification (RV) is a computing analysis paradigm based on observing a system at runtime to check its expected behavior. RV has emerged in recent years as a practical application of formal verification, and a less ad-hoc approach to conventional testing by building monitors from formal specifications.\nThere is a great potential applicability of RV beyond software reliability, if one allows monitors to interact back with the observed system, and generalizes to new domains beyond computers programs (like hardware, devices, cloud computing and even human centric systems). Given the European leadership in computer based industries, novel applications of RV to these areas can have an enormous impact in terms of the new class of designs enabled and their reliability and cost effectiveness.
EPSRC Doctoral Prize fellowship
1st June 2014 - 31st May 2015

EPSRC Knowledge Transfer Secondment Scheme
1 March 2013 - 28 Feb 2014

Ocean Observatories Initiative (Subcontract for OOI CI) Conversations and Governance
Nov 2011 - Nov 2013

NSF Grant

Dynamic Assurance based on Multiparty Session Types
Jul 2009 -

VMWare industry grant