-
Virtual Dosimetrists: A Radiotherapy Training "Flight Simulator"
Authors:
Skylar S. Gay,
Tucker Netherton,
Barbara Marquez,
Raymond Mumme,
Mary Gronberg,
Brent Parker,
Chelsea Pinnix,
Sanjay Shete,
Carlos Cardenas,
Laurence Court
Abstract:
Effective education in radiotherapy plan quality review requires a robust, regularly updated set of examples and the flexibility to demonstrate multiple possible planning approaches and their consequences. However, the current clinic-based paradigm does not support these needs. To address this, we have developed 'Virtual Dosimetrist' models that can both generate training examples of suboptimal tr…
▽ More
Effective education in radiotherapy plan quality review requires a robust, regularly updated set of examples and the flexibility to demonstrate multiple possible planning approaches and their consequences. However, the current clinic-based paradigm does not support these needs. To address this, we have developed 'Virtual Dosimetrist' models that can both generate training examples of suboptimal treatment plans and then allow trainees to improve the plan quality through simple natural language prompts, as if communicating with a dosimetrist. The dose generation and modification process is accurate, rapid, and requires only modest resources. This work is the first to combine dose distribution prediction with natural language processing; providing a robust pipeline for both generating suboptimal training plans and allowing trainees to practice their critical plan review and improvement skills that addresses the challenges of the current clinic-based paradigm.
△ Less
Submitted 14 May, 2025;
originally announced May 2025.
-
Special Delivery: Programming with Mailbox Types (Extended Version)
Authors:
Simon Fowler,
Duncan Paul Attard,
Franciszek Sowul,
Simon J. Gay,
Phil Trinder
Abstract:
The asynchronous and unidirectional communication model supported by mailboxes is a key reason for the success of actor languages like Erlang and Elixir for implementing reliable and scalable distributed systems. While many actors may send messages to some actor, only the actor may (selectively) receive from its mailbox. Although actors eliminate many of the issues stemming from shared memory conc…
▽ More
The asynchronous and unidirectional communication model supported by mailboxes is a key reason for the success of actor languages like Erlang and Elixir for implementing reliable and scalable distributed systems. While many actors may send messages to some actor, only the actor may (selectively) receive from its mailbox. Although actors eliminate many of the issues stemming from shared memory concurrency, they remain vulnerable to communication errors such as protocol violations and deadlocks.
Mailbox types are a novel behavioural type system for mailboxes first introduced for a process calculus by de'Liguoro and Padovani in 2018, which capture the contents of a mailbox as a commutative regular expression. Due to aliasing and nested evaluation contexts, moving from a process calculus to a programming language is challenging.
This paper presents Pat, the first programming language design incorporating mailbox types, and describes an algorithmic type system. We make essential use of quasi-linear typing to tame some of the complexity introduced by aliasing. Our algorithmic type system is necessarily co-contextual, achieved through a novel use of backwards bidirectional typing, and we prove it sound and complete with respect to our declarative type system. We implement a prototype type checker, and use it to demonstrate the expressiveness of Pat on a factory automation case study and a series of examples from the Savina actor benchmark suite.
△ Less
Submitted 22 June, 2023;
originally announced June 2023.
-
OpenKBP-Opt: An international and reproducible evaluation of 76 knowledge-based planning pipelines
Authors:
Aaron Babier,
Rafid Mahmood,
Binghao Zhang,
Victor G. L. Alves,
Ana Maria Barragán-Montero,
Joel Beaudry,
Carlos E. Cardenas,
Yankui Chang,
Zijie Chen,
Jaehee Chun,
Kelly Diaz,
Harold David Eraso,
Erik Faustmann,
Sibaji Gaj,
Skylar Gay,
Mary Gronberg,
Bingqi Guo,
Junjun He,
Gerd Heilemann,
Sanchit Hira,
Yuliang Huang,
Fuxin Ji,
Dashan Jiang,
Jean Carlo Jimenez Giraldo,
Hoyeon Lee
, et al. (34 additional authors not shown)
Abstract:
We establish an open framework for developing plan optimization models for knowledge-based planning (KBP) in radiotherapy. Our framework includes reference plans for 100 patients with head-and-neck cancer and high-quality dose predictions from 19 KBP models that were developed by different research groups during the OpenKBP Grand Challenge. The dose predictions were input to four optimization mode…
▽ More
We establish an open framework for developing plan optimization models for knowledge-based planning (KBP) in radiotherapy. Our framework includes reference plans for 100 patients with head-and-neck cancer and high-quality dose predictions from 19 KBP models that were developed by different research groups during the OpenKBP Grand Challenge. The dose predictions were input to four optimization models to form 76 unique KBP pipelines that generated 7600 plans. The predictions and plans were compared to the reference plans via: dose score, which is the average mean absolute voxel-by-voxel difference in dose a model achieved; the deviation in dose-volume histogram (DVH) criterion; and the frequency of clinical planning criteria satisfaction. We also performed a theoretical investigation to justify our dose mimicking models. The range in rank order correlation of the dose score between predictions and their KBP pipelines was 0.50 to 0.62, which indicates that the quality of the predictions is generally positively correlated with the quality of the plans. Additionally, compared to the input predictions, the KBP-generated plans performed significantly better (P<0.05; one-sided Wilcoxon test) on 18 of 23 DVH criteria. Similarly, each optimization model generated plans that satisfied a higher percentage of criteria than the reference plans. Lastly, our theoretical investigation demonstrated that the dose mimicking models generated plans that are also optimal for a conventional planning model. This was the largest international effort to date for evaluating the combination of KBP prediction and optimization models. In the interest of reproducibility, our data and code is freely available at https://github.com/ababier/open-kbp-opt.
△ Less
Submitted 16 February, 2022;
originally announced February 2022.
-
The Different Shades of Infinite Session Types
Authors:
Simon J. Gay,
Diogo Poças,
Vasco T. Vasconcelos
Abstract:
Many type systems include infinite types. In session type systems, which are the focus of this paper, infinite types are important because they allow the specification of communication protocols that are unbounded in time. Usually infinite session types are introduced as simple finite-state expressions $\mathsf{rec}\, X.T$ or by non-parametric equational definitions $X\doteq T$. Alternatively, som…
▽ More
Many type systems include infinite types. In session type systems, which are the focus of this paper, infinite types are important because they allow the specification of communication protocols that are unbounded in time. Usually infinite session types are introduced as simple finite-state expressions $\mathsf{rec}\, X.T$ or by non-parametric equational definitions $X\doteq T$. Alternatively, some systems of label- or value-dependent session types go beyond simple recursive types. However, leaving dependent types aside, there is a much richer world of infinite session types, ranging through various forms of parametric equational definitions, all the way to arbitrary infinite types in a coinductively defined space. We study infinite session types across a spectrum of shades of grey on the way to the bright light of general infinite types. We identify four points on the spectrum, characterised by different styles of equational definitions, and show that they form a strict hierarchy by establishing bidirectional correspondences with classes of automata: finite-state, 1-counter, pushdown and 2-counter. This allows us to establish decidability and undecidability results for the problems of type formation, type equivalence and duality in each class of types. We also consider previous work on context-free session types (and extend it to higher-order) and nested session types, and locate them on our spectrum of infinite types.
△ Less
Submitted 20 January, 2022;
originally announced January 2022.
-
Multiparty Session Types for Safe Runtime Adaptation in an Actor Language (Extended version)
Authors:
Paul Harvey,
Simon Fowler,
Ornela Dardha,
Simon J. Gay
Abstract:
Human fallibility, unpredictable operating environments, and the heterogeneity of hardware devices are driving the need for software to be able to adapt as seen in the Internet of Things or telecommunication networks. Unfortunately, mainstream programming languages do not readily allow a software component to sense and respond to its operating environment, by discovering, replacing, and communicat…
▽ More
Human fallibility, unpredictable operating environments, and the heterogeneity of hardware devices are driving the need for software to be able to adapt as seen in the Internet of Things or telecommunication networks. Unfortunately, mainstream programming languages do not readily allow a software component to sense and respond to its operating environment, by discovering, replacing, and communicating with components that are not part of the original system design, while maintaining static correctness guarantees. In particular, if a new component is discovered at runtime, there is no guarantee that its communication behaviour is compatible with existing components.
We address this problem by using multiparty session types with explicit connection actions, a type formalism used to model distributed communication protocols. By associating session types with software components, the discovery process can check protocol compatibility and, when required, correctly replace components without jeapordising safety.
We present the design and implementation of EnsembleS, the first actor-based language with adaptive features and a static session type system, and apply it to a case study based on an adaptive DNS server. We formalise the type system of EnsembleS and prove the safety of well-typed programs, making essential use of recent advances in non-classical multiparty session types.
△ Less
Submitted 14 May, 2021;
originally announced May 2021.
-
Duality of Session Types: The Final Cut
Authors:
Simon J. Gay,
Peter Thiemann,
Vasco T. Vasconcelos
Abstract:
Duality is a central concept in the theory of session types. Since a flaw was found in the original definition of duality for recursive types, several other definitions have been published. As their connection is not obvious, we compare the competing definitions, discuss tradeoffs, and prove some equivalences. Some of the results are mechanized in Agda.
Duality is a central concept in the theory of session types. Since a flaw was found in the original definition of duality for recursive types, several other definitions have been published. As their connection is not obvious, we compare the competing definitions, discuss tradeoffs, and prove some equivalences. Some of the results are mechanized in Agda.
△ Less
Submitted 2 April, 2020;
originally announced April 2020.
-
A Session Type System for Asynchronous Unreliable Broadcast Communication
Authors:
Dimitrios Kouzapas,
Ramunas Forsberg Gutkovas,
A. Laura Voinea,
Simon J. Gay
Abstract:
Session types are formal specifications of communication protocols, allowing protocol implementations to be verified by typechecking. Up to now, session type disciplines have assumed that the communication medium is reliable, with no loss of messages. However, unreliable broadcast communication is common in a wide class of distributed systems such as ad-hoc and wireless sensor networks. Often such…
▽ More
Session types are formal specifications of communication protocols, allowing protocol implementations to be verified by typechecking. Up to now, session type disciplines have assumed that the communication medium is reliable, with no loss of messages. However, unreliable broadcast communication is common in a wide class of distributed systems such as ad-hoc and wireless sensor networks. Often such systems have structured communication patterns that should be amenable to analysis by means of session types, but the necessary theory has not previously been developed. We introduce the Unreliable Broadcast Session Calculus, a process calculus with unreliable broadcast communication, and equip it with a session type system that we show is sound. We capture two common operations, broadcast and gather, inhabiting dual session types. Message loss may lead to non-synchronised session endpoints. To further account for unreliability we provide with an autonomous recovery mechanism that does not require acknowledgements from session participants. Our type system ensures soundness, safety, and progress between the synchronised endpoints within a session. We demonstrate the expressiveness of our framework by implementing Paxos, the textbook protocol for reaching consensus in an unreliable, asynchronous network.
△ Less
Submitted 2 August, 2024; v1 submitted 4 February, 2019;
originally announced February 2019.
-
REPETITA: Repeatable Experiments for Performance Evaluation of Traffic-Engineering Algorithms
Authors:
Steven Gay,
Pierre Schaus,
Stefano Vissicchio
Abstract:
In this paper, we propose a pragmatic approach to improve reproducibility of experimental analyses of traffic engineering (TE) algorithms, whose implementation, evaluation and comparison are currently hard to replicate. Our envisioned goal is to enable universally-checkable experiments of existing and future TE algorithms. We describe the design and implementation of REPETITA, a software framework…
▽ More
In this paper, we propose a pragmatic approach to improve reproducibility of experimental analyses of traffic engineering (TE) algorithms, whose implementation, evaluation and comparison are currently hard to replicate. Our envisioned goal is to enable universally-checkable experiments of existing and future TE algorithms. We describe the design and implementation of REPETITA, a software framework that implements common TE functions, automates experimental setup, and eases comparisons (in terms of solution quality, execution time, etc.) of TE algorithms. In its current version, REPETITA includes (i) a dataset for repeatable experiments, consisting of more than 250 real network topologies with complete bandwidth and delay information as well as associated traffic matrices; and (ii) the implementation of state-of-the-art algorithms for intra-domain TE with IGP weight tweaking and Segment Routing optimization. We showcase how our framework can successfully reproduce results described in the literature, and ease new analyses of qualitatively-diverse TE algorithms. We publicly release our REPETITA implementation, hoping that the community will consider it as a demonstration of feasibility, an incentive and an initial code basis for improving experiment reproducibility: Its plugin-oriented architecture indeed makes REPETITA easy to extend with new datasets, algorithms, TE primitives and analyses. We therefore invite the research community to use and contribute to our released code and dataset.
△ Less
Submitted 24 October, 2017;
originally announced October 2017.
-
Liveness for Verification
Authors:
Roly Perera,
Simon J. Gay
Abstract:
We explore the use of liveness for interactive program verification for a simple concurrent object language. Our experimental IDE integrates two (formally dual) kinds of continuous testing into the development environment: compatibility-checking, which verifies an object's use of other objects, and compliance-checking, which verifies an object's claim to refine the behaviour of another object. Sou…
▽ More
We explore the use of liveness for interactive program verification for a simple concurrent object language. Our experimental IDE integrates two (formally dual) kinds of continuous testing into the development environment: compatibility-checking, which verifies an object's use of other objects, and compliance-checking, which verifies an object's claim to refine the behaviour of another object. Source code errors highlighted by the IDE are not static type errors but the reflection back to the source of runtime errors that occur in some execution of the system. We demonstrate our approach, and discuss opportunities and challenges.
△ Less
Submitted 14 September, 2016;
originally announced September 2016.
-
Behavioural Prototypes
Authors:
Roly Perera,
Simon J. Gay
Abstract:
We sketch a simple language of concurrent objects which explores the design space between type systems and continuous testing. In our language, programs are collections of communicating automata checked automatically for multiparty compatibility. This property, taken from the session types literature but here applied to terms rather than types, guarantees that no state-related errors arise during…
▽ More
We sketch a simple language of concurrent objects which explores the design space between type systems and continuous testing. In our language, programs are collections of communicating automata checked automatically for multiparty compatibility. This property, taken from the session types literature but here applied to terms rather than types, guarantees that no state-related errors arise during execution: no object gets stuck because it was sent the wrong message, and every message is processed.
△ Less
Submitted 3 September, 2016;
originally announced September 2016.
-
Multiparty Compatibility for Concurrent Objects
Authors:
Roly Perera,
Julien Lange,
Simon J. Gay
Abstract:
Objects and actors are communicating state machines, offering and consuming different services at different points in their lifecycle. Two complementary challenges arise when programming such systems. When objects interact, their state machines must be "compatible", so that services are requested only when they are available. Dually, when objects refine other objects, their state machines must be…
▽ More
Objects and actors are communicating state machines, offering and consuming different services at different points in their lifecycle. Two complementary challenges arise when programming such systems. When objects interact, their state machines must be "compatible", so that services are requested only when they are available. Dually, when objects refine other objects, their state machines must be "compliant", so that services are honoured whenever they are promised.
In this paper we show how the idea of multiparty compatibility from the session types literature can be applied to both of these problems. We present an untyped language in which concurrent objects are checked automatically for compatibility and compliance. For simple objects, checking can be exhaustive and has the feel of a type system. More complex objects can be partially validated via test cases, leading to a methodology closer to continuous testing. Our proof-of-concept implementation is limited in some important respects, but demonstrates the potential value of the approach and the relationship to existing software development practices.
△ Less
Submitted 19 June, 2016;
originally announced June 2016.
-
Proceedings Eighth International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software
Authors:
Simon Gay,
Jade Alglave
Abstract:
PLACES 2015 (full title: Programming Language Approaches to Concurrency- and Communication-Centric Software) is the eighth edition of the PLACES workshop series. After the first PLACES, which was affiliated to DisCoTec in 2008, the workshop has been part of ETAPS every year since 2009 and is now an established part of the ETAPS satellite events. PLACES 2015 was held on 18th April in London, UK.…
▽ More
PLACES 2015 (full title: Programming Language Approaches to Concurrency- and Communication-Centric Software) is the eighth edition of the PLACES workshop series. After the first PLACES, which was affiliated to DisCoTec in 2008, the workshop has been part of ETAPS every year since 2009 and is now an established part of the ETAPS satellite events. PLACES 2015 was held on 18th April in London, UK.
The workshop series was started in order to promote the application of novel programming language ideas to the increasingly important problem of developing software for systems in which concurrency and communication are intrinsic aspects. This includes software for both multi-core systems and large-scale distributed and/or service-oriented systems. The scope of PLACES includes new programming language features, whole new programming language designs, new type systems, new semantic approaches, new program analysis techniques, and new implementation mechanisms.
This volume consists of revised versions of the papers that were presented at the workshop.
△ Less
Submitted 9 February, 2016;
originally announced February 2016.
-
Verification of Linear Optical Quantum Computing using Quantum Process Calculus
Authors:
Sonja Franke-Arnold,
Simon J. Gay,
Ittoop Vergheese Puthoor
Abstract:
We explain the use of quantum process calculus to describe and analyse linear optical quantum computing (LOQC). The main idea is to define two processes, one modelling a linear optical system and the other expressing a specification, and prove that they are behaviourally equivalent. We extend the theory of behavioural equivalence in the process calculus Communicating Quantum Processes (CQP) to inc…
▽ More
We explain the use of quantum process calculus to describe and analyse linear optical quantum computing (LOQC). The main idea is to define two processes, one modelling a linear optical system and the other expressing a specification, and prove that they are behaviourally equivalent. We extend the theory of behavioural equivalence in the process calculus Communicating Quantum Processes (CQP) to include multiple particles (namely photons) as information carriers, described by Fock states or number states. We summarise the theory in this paper, including the crucial result that equivalence is a congruence, meaning that it is preserved by embedding in any context. In previous work, we have used quantum process calculus to model LOQC but without verifying models against specifications. In this paper, for the first time, we are able to carry out verification. We illustrate this approach by describing and verifying two models of an LOQC CNOT gate.
△ Less
Submitted 6 August, 2014;
originally announced August 2014.
-
Session Types as Generic Process Types
Authors:
Simon J. Gay,
Nils Gesbert,
António Ravara
Abstract:
Behavioural type systems ensure more than the usual safety guarantees of static analysis. They are based on the idea of "types-as-processes", providing dedicated type algebras for particular properties, ranging from protocol compatibility to race-freedom, lock-freedom, or even responsiveness. Two successful, although rather different, approaches, are session types and process types. The former all…
▽ More
Behavioural type systems ensure more than the usual safety guarantees of static analysis. They are based on the idea of "types-as-processes", providing dedicated type algebras for particular properties, ranging from protocol compatibility to race-freedom, lock-freedom, or even responsiveness. Two successful, although rather different, approaches, are session types and process types. The former allows to specify and verify (distributed) communication protocols using specific type (proof) systems; the latter allows to infer from a system specification a process abstraction on which it is simpler to verify properties, using a generic type (proof) system. What is the relationship between these approaches? Can the generic one subsume the specific one? At what price? And can the former be used as a compiler for the latter? The work presented herein is a step towards answers to such questions. Concretely, we define a stepwise encoding of a pi-calculus with sessions and session types (the system of Gay and Hole) into a pi-calculus with process types (the Generic Type System of Igarashi and Kobayashi). We encode session type environments, polarities (which distinguish session channels end-points), and labelled sums. We show forward and reverse operational correspondences for the encodings, as well as typing correspondences. To faithfully encode session subtyping in process types subtyping, one needs to add to the target language record constructors and new subtyping rules. In conclusion, the programming convenience of session types as protocol abstractions can be combined with the simplicity and power of the pi-calculus, taking advantage in particular of the framework provided by the Generic Type System.
△ Less
Submitted 6 August, 2014;
originally announced August 2014.
-
Session Types for Broadcasting
Authors:
Dimitrios Kouzapas,
Ramūnas Gutkovas,
Simon J. Gay
Abstract:
Up to now session types have been used under the assumptions of point to point communication, to ensure the linearity of session endpoints, and reliable communication, to ensure send/receive duality. In this paper we define a session type theory for broadcast communication semantics that by definition do not assume point to point and reliable communication. Our session framework lies on top of the…
▽ More
Up to now session types have been used under the assumptions of point to point communication, to ensure the linearity of session endpoints, and reliable communication, to ensure send/receive duality. In this paper we define a session type theory for broadcast communication semantics that by definition do not assume point to point and reliable communication. Our session framework lies on top of the parametric framework of broadcasting psi-calculi, giving insights on developing session types within a parametric framework. Our session type theory enjoys the properties of soundness and safety. We further believe that the solutions proposed will eventually provide a deeper understanding of how session types principles should be applied in the general case of communication semantics.
△ Less
Submitted 13 June, 2014;
originally announced June 2014.
-
Automated Verification of Quantum Protocols by Equivalence Checking
Authors:
Ebrahim Ardeshir-Larijani,
Simon J. Gay,
Rajagopal Nagarajan
Abstract:
In this paper we introduce a technique and a tool for formal verification of various quantum information processing protocols. The tool uses stabilizer formalism and is capable of representing concurrent quantum protocol, thus is more expressive than quantum circuits. We also report on experimental results of using our Quantum Equivalence Checker (QEC) to analyse a range of quantum information pro…
▽ More
In this paper we introduce a technique and a tool for formal verification of various quantum information processing protocols. The tool uses stabilizer formalism and is capable of representing concurrent quantum protocol, thus is more expressive than quantum circuits. We also report on experimental results of using our Quantum Equivalence Checker (QEC) to analyse a range of quantum information processing protocols.
△ Less
Submitted 20 December, 2013;
originally announced December 2013.
-
Application of Quantum Process Calculus to Higher Dimensional Quantum Protocols
Authors:
Simon J. Gay,
Ittoop Vergheese Puthoor
Abstract:
We describe the use of quantum process calculus to describe and analyze quantum communication protocols, following the successful field of formal methods from classical computer science. We have extended the quantum process calculus to describe d-dimensional quantum systems, which has not been done before. We summarise the necessary theory in the generalisation of quantum gates and Bell states and…
▽ More
We describe the use of quantum process calculus to describe and analyze quantum communication protocols, following the successful field of formal methods from classical computer science. We have extended the quantum process calculus to describe d-dimensional quantum systems, which has not been done before. We summarise the necessary theory in the generalisation of quantum gates and Bell states and use the theory to apply the quantum process calculus CQP to quantum protocols, namely qudit teleportation and superdense coding.
△ Less
Submitted 31 July, 2014; v1 submitted 12 March, 2013;
originally announced March 2013.
-
Proceedings Fifth Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software
Authors:
Simon Gay,
Paul Kelly
Abstract:
PLACES 2012 (full title: Programming Language Approaches to Concurrency- and Communication-Centric Software) is the fifth edition of the PLACES workshop series. After the first PLACES, which was affiliated to DisCoTec in 2008, the workshop has been part of ETAPS every year since 2009 and is now an established part of the ETAPS satellite events. PLACES 2012 was held on 31st March in Tallinn, Estoni…
▽ More
PLACES 2012 (full title: Programming Language Approaches to Concurrency- and Communication-Centric Software) is the fifth edition of the PLACES workshop series. After the first PLACES, which was affiliated to DisCoTec in 2008, the workshop has been part of ETAPS every year since 2009 and is now an established part of the ETAPS satellite events. PLACES 2012 was held on 31st March in Tallinn, Estonia.
The workshop series was started in order to promote the application of novel programming language ideas to the increasingly important problem of developing software for systems in which concurrency and communication are intrinsic aspects. This includes software for both multi-core systems and large-scale distributed and/or service-oriented systems. The scope of PLACES includes new programming language features, whole new programming language designs, new type systems, new semantic approaches, new program analysis techniques, and new implementation mechanisms.
This year's call for papers attracted 17 submissions, from which the programme committee selected 10 papers for presentation at the workshop. After the workshop, all of the authors were invited to produce revised versions of their papers for inclusion in the EPTCS proceedings. The authors of six papers accepted the invitation, and those papers constitute the present volume.
△ Less
Submitted 23 February, 2013;
originally announced February 2013.
-
Analysis of a Quantum Error Correcting Code using Quantum Process Calculus
Authors:
Timothy A. S. Davidson,
Simon J. Gay,
Rajagopal Nagarajan,
Ittoop Vergheese Puthoor
Abstract:
We describe the use of quantum process calculus to describe and analyze quantum communication protocols, following the successful field of formal methods from classical computer science. The key idea is to define two systems, one modelling a protocol and one expressing a specification, and prove that they are behaviourally equivalent. We summarize the necessary theory in the process calculus CQP,…
▽ More
We describe the use of quantum process calculus to describe and analyze quantum communication protocols, following the successful field of formal methods from classical computer science. The key idea is to define two systems, one modelling a protocol and one expressing a specification, and prove that they are behaviourally equivalent. We summarize the necessary theory in the process calculus CQP, including the crucial result that equivalence is a congruence, meaning that it is preserved by embedding in any context. We illustrate the approach by analyzing two versions of a quantum error correction system.
△ Less
Submitted 1 October, 2012;
originally announced October 2012.
-
Modular session types for objects
Authors:
Simon J. Gay,
Nils Gesbert,
António Ravara,
Vasco T. Vasconcelos
Abstract:
Session types allow communication protocols to be specified type-theoretically so that protocol implementations can be verified by static type checking. We extend previous work on session types for distributed object-oriented languages in three ways. (1) We attach a session type to a class definition, to specify the possible sequences of method calls. (2) We allow a session type (protocol) impleme…
▽ More
Session types allow communication protocols to be specified type-theoretically so that protocol implementations can be verified by static type checking. We extend previous work on session types for distributed object-oriented languages in three ways. (1) We attach a session type to a class definition, to specify the possible sequences of method calls. (2) We allow a session type (protocol) implementation to be modularized, i.e. partitioned into separately-callable methods. (3) We treat session-typed communication channels as objects, integrating their session types with the session types of classes. The result is an elegant unification of communication channels and their session types, distributed object-oriented programming, and a form of typestate supporting non-uniform objects, i.e. objects that dynamically change the set of available methods. We define syntax, operational se-mantics, a sound type system, and a sound and complete type checking algorithm for a small distributed class-based object-oriented language with structural subtyping. Static typing guarantees that both sequences of messages on channels, and sequences of method calls on objects, conform to type-theoretic specifications, thus ensuring type-safety. The language includes expected features of session types, such as delegation, and expected features of object-oriented programming, such as encapsulation of local state.
△ Less
Submitted 23 December, 2015; v1 submitted 24 May, 2012;
originally announced May 2012.
-
Stabilizer States as a Basis for Density Matrices
Authors:
Simon J. Gay
Abstract:
We show that the space of density matrices for n-qubit states, considered as a (2^n)^2 dimensional real vector space, has a basis consisting of density matrices of stabilizer states. We describe an application of this result to automated verification of quantum protocols.
We show that the space of density matrices for n-qubit states, considered as a (2^n)^2 dimensional real vector space, has a basis consisting of density matrices of stabilizer states. We describe an application of this result to automated verification of quantum protocols.
△ Less
Submitted 9 December, 2011;
originally announced December 2011.
-
Formal Analysis of Quantum Systems using Process Calculus
Authors:
Timothy A. S. Davidson,
Simon J. Gay,
Rajagopal Nagarajan
Abstract:
Quantum communication and cryptographic protocols are well on the way to becoming an important practical technology. Although a large amount of successful research has been done on proving their correctness, most of this work does not make use of familiar techniques from formal methods, such as formal logics for specification, formal modelling languages, separation of levels of abstraction, and co…
▽ More
Quantum communication and cryptographic protocols are well on the way to becoming an important practical technology. Although a large amount of successful research has been done on proving their correctness, most of this work does not make use of familiar techniques from formal methods, such as formal logics for specification, formal modelling languages, separation of levels of abstraction, and compositional analysis. We argue that these techniques will be necessary for the analysis of large-scale systems that combine quantum and classical components, and summarize the results of initial investigation using behavioural equivalence in process calculus. This paper is a summary of Simon Gay's invited talk at ICE'11.
△ Less
Submitted 1 August, 2011;
originally announced August 2011.
-
Proceedings Second International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software
Authors:
Alastair R. Beresford,
Simon Gay
Abstract:
The Second International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES) was co-located with ETAPS 2009 in the city of York, England. The workshop took place on Sunday 22nd March 2009. The workshop focused on the challenges raised by the changing landscape of computer software. Traditionally, most software was written for a single computer w…
▽ More
The Second International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES) was co-located with ETAPS 2009 in the city of York, England. The workshop took place on Sunday 22nd March 2009. The workshop focused on the challenges raised by the changing landscape of computer software. Traditionally, most software was written for a single computer with one CPU. However applications on the web today are built using numerous interacting services deployed on across many machines; soon off-the-shelf CPUs will host thousands of cores, and sensor networks will be composed from a large number of processing units. Many normal applications will soon need to make effective use of thousands of computing nodes. At some level of granularity, computation in such systems will be inherently concurrent and communication-centred.
The development of effective programming methodologies for the coming computing paradigm demands exploration and understanding of a wide variety of ideas and techniques. This workshop offered a forum where researchers from different fields could exchange new ideas on one of the central challenges for programming in the near future, the development of programming methodologies and infrastructures where concurrency and distribution are the norm rather than a marginal concern.
△ Less
Submitted 6 February, 2010;
originally announced February 2010.
-
Probabilistic Model--Checking of Quantum Protocols
Authors:
Simon Gay,
Rajagopal Nagarajan,
Nikolaos Papanikolaou
Abstract:
We establish fundamental and general techniques for formal verification of quantum protocols. Quantum protocols are novel communication schemes involving the use of quantum-mechanical phenomena for representation, storage and transmission of data. As opposed to quantum computers, quantum communication systems can and have been implemented using present-day technology; therefore, the ability to m…
▽ More
We establish fundamental and general techniques for formal verification of quantum protocols. Quantum protocols are novel communication schemes involving the use of quantum-mechanical phenomena for representation, storage and transmission of data. As opposed to quantum computers, quantum communication systems can and have been implemented using present-day technology; therefore, the ability to model and analyse such systems rigorously is of primary importance.
While current analyses of quantum protocols use a traditional mathematical approach and require considerable understanding of the underlying physics, we argue that automated verification techniques provide an elegant alternative. We demonstrate these techniques through the use of PRISM, a probabilistic model-checking tool. Our approach is conceptually simpler than existing proofs, and allows us to disambiguate protocol definitions and assess their properties. It also facilitates detailed analyses of actual implemented systems. We illustrate our techniques by modelling a selection of quantum protocols (namely superdense coding, quantum teleportation, and quantum error correction) and verifying their basic correctness properties. Our results provide a foundation for further work on modelling and analysing larger systems such as those used for quantum cryptography, in which basic protocols are used as components.
△ Less
Submitted 5 October, 2005; v1 submitted 1 April, 2005;
originally announced April 2005.
-
An Automated Analysis of the Security of Quantum Key Distribution
Authors:
Rajagopal Nagarajan,
Nikolaos Papanikolaou,
Garry Bowen,
Simon Gay
Abstract:
This paper discusses the use of computer-aided verification as a practical means for analysing quantum information systems; specifically, the BB84 protocol for quantum key distribution is examined using this method. This protocol has been shown to be unconditionally secure against all attacks in an information-theoretic setting, but the relevant security proof requires a thorough understanding o…
▽ More
This paper discusses the use of computer-aided verification as a practical means for analysing quantum information systems; specifically, the BB84 protocol for quantum key distribution is examined using this method. This protocol has been shown to be unconditionally secure against all attacks in an information-theoretic setting, but the relevant security proof requires a thorough understanding of the formalism of quantum mechanics and is not easily adaptable to practical scenarios. Our approach is based on probabilistic model-checking; we have used the PRISM model-checker to show that, as the number of qubits transmitted in BB84 is increased, the equivocation of the eavesdropper with respect to the channel decreases exponentially. We have also shown that the probability of detecting the presence of an eavesdropper increases exponentially with the number of qubits. The results presented here are a testament to the effectiveness of the model-checking approach for systems where analytical solutions may not be possible or plausible.
△ Less
Submitted 9 February, 2005;
originally announced February 2005.
