MobilityReadingGroup

π-calculus, Session Types research at Imperial College

Research Grants

Border Patrol: Improving Smart Device Security through Type-Aware Systems Design
Feb 2017 - Jan 2022
EP-N028201-1

http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/N028201/1
Turtles: Protocol-Based Foundations for Distributed Multiagent Systems
Nov 2016 - Oct 2021
EP-N027833-1

Related grant: EP/N027965/1

http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/N027833/1
Exploiting Parallelism through Type Transformations for Hybrid Manycore Systems
Oct 2013 - Sep 2018
EP-L00058X-1

http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/L00058X/1
From Data Types to Session Types - A Basis for Concurrency and Distribution
May 2013 - May 2019
EP-K034413-1

http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/K034413/1
Conversation-Based Governance for Distributed Systems by Multiparty Session Types
Jun 2013 - Jun 2018
EP-K011715-1

http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/K011715/1
Application Customisation: Enhancing Design Quality and Developer Productivity
Dec 2016 - Nov 2021
EP-P010040-1

http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/P010040/1
EU FP7 FET OpenX: UpScale
Feb 2014 - Jan 2017
FP7-upscale

http://upscale-project.eu/
COST Action IC1201 BETTY
Oct 2012 - Oct 2016
ic1201

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.

http://www.cost.eu/COST_Actions/ict/Actions/IC1201
COST Action IC1405 Reversible computation
July 2015 -
ic1405

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.

http://www.cost.eu/COST_Actions/ict/Actions/IC1405
COST Action IC1402 ARVI
April 2015 -
ic1402

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.

http://www.cost.eu/COST_Actions/ict/Actions/IC1402
EPSRC Doctoral Prize fellowship
1st June 2014 - 31st May 2015
doctoral-prize-dk

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

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

NSF Grant

Dynamic Assurance based on Multiparty Session Types
Jul 2009 -
vmware

VMWare industry grant