-
Brewer-Nash Scrutinised: Mechanised Checking of Policies featuring Write Revocation
Authors:
Alfredo Capozucca,
Maximiliano Cristiá,
Ross Horne,
Ricardo Katz
Abstract:
This paper revisits the Brewer-Nash security policy model inspired by ethical Chinese Wall policies. We draw attention to the fact that write access can be revoked in the Brewer-Nash model. The semantics of write access were underspecified originally, leading to multiple interpretations for which we provide a modern operational semantics. We go on to modernise the analysis of information flow in t…
▽ More
This paper revisits the Brewer-Nash security policy model inspired by ethical Chinese Wall policies. We draw attention to the fact that write access can be revoked in the Brewer-Nash model. The semantics of write access were underspecified originally, leading to multiple interpretations for which we provide a modern operational semantics. We go on to modernise the analysis of information flow in the Brewer-Nash model, by adopting a more precise definition adapted from Kessler. For our modernised reformulation, we provide full mechanised coverage for all theorems proposed by Brewer & Nash. Most theorems are established automatically using the tool {log} with the exception of a theorem regarding information flow, which combines a lemma in {log} with a theorem mechanised in Coq. Having covered all theorems originally posed by Brewer-Nash, achieving modern precision and mechanisation, we propose this work as a step towards a methodology for automated checking of more complex security policy models.
△ Less
Submitted 28 May, 2024; v1 submitted 20 May, 2024;
originally announced May 2024.
-
Thermal Earth Model for the Conterminous United States Using an Interpolative Physics-Informed Graph Neural Network (InterPIGNN)
Authors:
Mohammad J. Aljubran,
Roland N. Horne
Abstract:
This study presents a data-driven spatial interpolation algorithm based on physics-informed graph neural networks used to develop national temperature-at-depth maps for the conterminous United States. The model was trained to approximately satisfy the three-dimensional heat conduction law by simultaneously predicting subsurface temperature, surface heat flow, and rock thermal conductivity. In addi…
▽ More
This study presents a data-driven spatial interpolation algorithm based on physics-informed graph neural networks used to develop national temperature-at-depth maps for the conterminous United States. The model was trained to approximately satisfy the three-dimensional heat conduction law by simultaneously predicting subsurface temperature, surface heat flow, and rock thermal conductivity. In addition to bottomhole temperature measurements, we incorporated other physical quantities as model inputs, such as depth, geographic coordinates, elevation, sediment thickness, magnetic anomaly, gravity anomaly, gamma-ray flux of radioactive elements, seismicity, and electric conductivity. We constructed surface heat flow, and temperature and thermal conductivity predictions for depths of 0-7 km at an interval of 1 km with spatial resolution of 18 km$^2$ per grid cell. Our model showed superior temperature, surface heat flow and thermal conductivity mean absolute errors of 4.8° C, 5.817 mW/m$^2$ and 0.022 W/(C-m)$, respectively. The predictions were visualized in two-dimensional spatial maps across the modeled depths. This thorough modeling of the Earth's thermal processes is crucial to understanding subsurface phenomena and exploiting natural underground resources.
△ Less
Submitted 14 March, 2024;
originally announced March 2024.
-
Provably Unlinkable Smart Card-based Payments
Authors:
Sergiu Bursuc,
Ross Horne,
Sjouke Mauw,
Semen Yurkov
Abstract:
The most prevalent smart card-based payment method, EMV, currently offers no privacy to its users. Transaction details and the card number are sent in cleartext, enabling the profiling and tracking of cardholders. Since public awareness of privacy issues is growing and legislation, such as GDPR, is emerging, we believe it is necessary to investigate the possibility of making payments anonymous and…
▽ More
The most prevalent smart card-based payment method, EMV, currently offers no privacy to its users. Transaction details and the card number are sent in cleartext, enabling the profiling and tracking of cardholders. Since public awareness of privacy issues is growing and legislation, such as GDPR, is emerging, we believe it is necessary to investigate the possibility of making payments anonymous and unlinkable without compromising essential security guarantees and functional properties of EMV. This paper draws attention to trade-offs between functional and privacy requirements in the design of such a protocol. We present the UTX protocol - an enhanced payment protocol satisfying such requirements, and we formally certify key security and privacy properties using techniques based on the applied pi-calculus.
△ Less
Submitted 6 September, 2023;
originally announced September 2023.
-
A Logical Account of Subty** for Session Types
Authors:
Ross Horne,
Luca Padovani
Abstract:
We study the notion of subty** for session types in a logical setting, where session types are propositions of multiplicative/additive linear logic extended with least and greatest fixed points. The resulting subty** relation admits a simple characterization that can be roughly spelled out as the following lapalissade: every session type is larger than the smallest session type and smaller tha…
▽ More
We study the notion of subty** for session types in a logical setting, where session types are propositions of multiplicative/additive linear logic extended with least and greatest fixed points. The resulting subty** relation admits a simple characterization that can be roughly spelled out as the following lapalissade: every session type is larger than the smallest session type and smaller than the largest session type. At the same time, we observe that this subty**, unlike traditional ones, preserves termination in addition to the usual safety properties of sessions. We present a calculus of sessions that adopts this subty** relation and we show that subty**, while useful in practice, is superfluous in the theory: every use of subty** can be "compiled away" via a coercion semantics.
△ Less
Submitted 13 April, 2023;
originally announced April 2023.
-
Regulating trusted autonomous systems in Australia
Authors:
Rachel Horne,
Tom Putland,
Mark Brady
Abstract:
Australia is a leader in autonomous systems technology, particularly in the mining industry, borne from necessity in a geographically dispersed and complex natural environment. Increasingly advanced autonomous systems are becoming more prevalent in Australia, particularly as the safety, environmental and efficiency benefits become better understood, and the increasing sophistication of technology…
▽ More
Australia is a leader in autonomous systems technology, particularly in the mining industry, borne from necessity in a geographically dispersed and complex natural environment. Increasingly advanced autonomous systems are becoming more prevalent in Australia, particularly as the safety, environmental and efficiency benefits become better understood, and the increasing sophistication of technology improves capability and availability. Increasing use of these systems, including in the maritime domain and air domain, is placing pressure on the national safety regulators, who must either continue to apply their traditional regulatory approach requiring exemptions to enable operation of emerging technology, or seize the opportunity to put in place an agile and adaptive approach better suited to the rapid developments of the twenty first century. In Australia the key national safety regulators have demonstrated an appetite for working with industry to facilitate innovation, but their limited resources mean progress is slow. There is a critical role to be played by third parties from industry, government, and academia who can work together to develop, test and publish new assurance and accreditation frameworks for trusted autonomous systems, and assist in the transition to an adaptive and agile regulatory philosophy. This is necessary to ensure the benefits of autonomous systems can be realised, without compromising safety. This paper will identify the growing use cases for autonomous systems in Australia, in the maritime, air and land domains, assess the current regulatory framework, argue that Australia's regulatory approach needs to become more agile and anticipatory, and investigate how third party projects could positively impact the assurance and accreditation process for autonomous systems in the future.
△ Less
Submitted 7 February, 2023;
originally announced February 2023.
-
Assessing the Solid Protocol in Relation to Security & Privacy Obligations
Authors:
Christian Esposito,
Olaf Hartig,
Ross Horne,
Chang Sun
Abstract:
The Solid specification aims to empower data subjects by giving them direct access control over their data across multiple applications. As governments are manifesting their interest in this framework for citizen empowerment and e-government services, security and privacy represent pivotal issues to be addressed. By analyzing the relevant legislation, notably GDPR, and international standards, nam…
▽ More
The Solid specification aims to empower data subjects by giving them direct access control over their data across multiple applications. As governments are manifesting their interest in this framework for citizen empowerment and e-government services, security and privacy represent pivotal issues to be addressed. By analyzing the relevant legislation, notably GDPR, and international standards, namely ISO/IEC 27001:2011 and 15408, we formulate the primary security and privacy requirements for such a framework. Furthermore, we survey the current Solid protocol specifications regarding how they cover the highlighted requirements, and draw attention to potential gaps between the specifications and requirements. We also point out the contribution of recent academic work presenting novel approaches to increase the security and privacy degree provided by the Solid project. This paper has a twofold contribution to improve user awareness of how Solid can help protect their data and to present possible future research lines on Solid security and privacy enhancements.
△ Less
Submitted 15 October, 2022;
originally announced October 2022.
-
Bisimulations Respecting Duration and Causality for the Non-interleaving Applied $π$-Calculus
Authors:
Clément Aubert,
Ross Horne,
Christian Johansen
Abstract:
This paper shows how we can make use of an asynchronous transition system, whose transitions are labelled with events and which is equipped with a notion of independence of events, to define non-interleaving semantics for the applied $π$-calculus. The most important notions we define are: Start-Termination or ST-bisimilarity, preserving duration of events; and History-Preserving or HP- bisimilarit…
▽ More
This paper shows how we can make use of an asynchronous transition system, whose transitions are labelled with events and which is equipped with a notion of independence of events, to define non-interleaving semantics for the applied $π$-calculus. The most important notions we define are: Start-Termination or ST-bisimilarity, preserving duration of events; and History-Preserving or HP- bisimilarity, preserving causality. We point out that corresponding similarity preorders expose clearly distinctions between these semantics. We draw particular attention to the distinguishing power of HP failure similarity, and discuss how it affects the attacker threat model against which we verify security and privacy properties. We also compare existing notions of located bisimilarity to the definitions we introduce.
△ Less
Submitted 6 September, 2022;
originally announced September 2022.
-
Unlinkability of an Improved Key Agreement Protocol for EMV 2nd Gen Payments
Authors:
Ross Horne,
Sjouke Mauw,
Semen Yurkov
Abstract:
To address known privacy problems with the EMV standard, EMVCo have proposed a Blinded Diffie-Hellman key establishment protocol, which is intended to be part of a future 2nd Gen EMV protocol. We point out that active attackers were not previously accounted for in the privacy requirements of this proposal protocol, and demonstrate that an active attacker can compromise unlinkability within a dista…
▽ More
To address known privacy problems with the EMV standard, EMVCo have proposed a Blinded Diffie-Hellman key establishment protocol, which is intended to be part of a future 2nd Gen EMV protocol. We point out that active attackers were not previously accounted for in the privacy requirements of this proposal protocol, and demonstrate that an active attacker can compromise unlinkability within a distance of 100cm. Here, we adopt a strong definition of unlinkability that does account for active attackers and propose an enhancement of the protocol proposed by EMVCo. We prove that our protocol does satisfy strong unlinkability, while preserving authentication.
△ Less
Submitted 22 June, 2022; v1 submitted 5 May, 2021;
originally announced May 2021.
-
Assuming Just Enough Fairness to make Session Types Complete for Lock-freedom
Authors:
Rob van Glabbeek,
Peter Höfner,
Ross Horne
Abstract:
We investigate how different fairness assumptions affect results concerning lock-freedom, a typical liveness property targeted by session type systems. We fix a minimal session calculus and systematically take into account all known fairness assumptions, thereby identifying precisely three interesting and semantically distinct notions of lock-freedom, all of which having a sound session type syste…
▽ More
We investigate how different fairness assumptions affect results concerning lock-freedom, a typical liveness property targeted by session type systems. We fix a minimal session calculus and systematically take into account all known fairness assumptions, thereby identifying precisely three interesting and semantically distinct notions of lock-freedom, all of which having a sound session type system. We then show that, by using a general merge operator in an otherwise standard approach to global session types, we obtain a session type system complete for the strongest amongst those notions of lock-freedom, which assumes only justness of execution paths, a minimal fairness assumption for concurrent systems.
△ Less
Submitted 29 April, 2021;
originally announced April 2021.
-
Trust and Safety
Authors:
S. K. Devitt,
R. Horne,
Z. Assaad,
E. Broad,
H. Kurniawati,
B. Cardier,
A. Scott,
S. Lazar,
M. Gould,
C. Adamson,
C. Karl,
F. Schrever,
S. Keay,
K. Tranter,
E. Shellshear,
D. Hunter,
M. Brady,
T. Putland
Abstract:
Robotics in Australia have a long history of conforming with safety standards and risk managed practices. This chapter articulates the current state of trust and safety in robotics including society's expectations, safety management systems and system safety as well as emerging issues and methods for ensuring safety in increasingly autonomous robotics. The future of trust and safety will combine s…
▽ More
Robotics in Australia have a long history of conforming with safety standards and risk managed practices. This chapter articulates the current state of trust and safety in robotics including society's expectations, safety management systems and system safety as well as emerging issues and methods for ensuring safety in increasingly autonomous robotics. The future of trust and safety will combine standards with iterative, adaptive and responsive regulatory and assurance methods for diverse applications of robotics, autonomous systems and artificial intelligence (RAS-AI). Robotics will need novel technical and social approaches to achieve assurance, particularly for game-changing innovations. The ability for users to easily update algorithms and software, which alters the performance of a system, implies that traditional machine assurance performed prior to deployment or sale, will no longer be viable. Moreover, the high frequency of updates implies that traditional certification that requires substantial time will no longer be practical. To alleviate these difficulties, automation of assurance will likely be needed; something like 'ASsurance-as-a-Service' (ASaaS), where APIs constantly ** RAS-AI to ensure abidance with various rules, frameworks and behavioural expectations. There are exceptions to this, such as in contested or communications denied environments, or in underground or undersea mining; and these systems need their own risk assessments and limitations imposed. Indeed, self-monitors are already operating within some systems. To ensure safe operations of future robotics systems, Australia needs to invest in RAS-AI assurance research, stakeholder engagement and continued development and refinement of robust frameworks, methods, guidelines and policy in order to educate and prepare its technology developers, certifiers, and general population.
△ Less
Submitted 13 April, 2021;
originally announced April 2021.
-
An Analytic Propositional Proof System on Graphs
Authors:
Matteo Acclavio,
Ross Horne,
Lutz Straßburger
Abstract:
In this paper we present a proof system that operates on graphs instead of formulas. Starting from the well-known relationship between formulas and cographs, we drop the cograph-conditions and look at arbitrary undirected) graphs. This means that we lose the tree structure of the formulas corresponding to the cographs, and we can no longer use standard proof theoretical methods that depend on that…
▽ More
In this paper we present a proof system that operates on graphs instead of formulas. Starting from the well-known relationship between formulas and cographs, we drop the cograph-conditions and look at arbitrary undirected) graphs. This means that we lose the tree structure of the formulas corresponding to the cographs, and we can no longer use standard proof theoretical methods that depend on that tree structure. In order to overcome this difficulty, we use a modular decomposition of graphs and some techniques from deep inference where inference rules do not rely on the main connective of a formula. For our proof system we show the admissibility of cut and a generalisation of the splitting property. Finally, we show that our system is a conservative extension of multiplicative linear logic with mix, and we argue that our graphs form a notion of generalised connective.
△ Less
Submitted 20 October, 2022; v1 submitted 2 December, 2020;
originally announced December 2020.
-
Discovering ePassport Vulnerabilities using Bisimilarity
Authors:
Ross Horne,
Sjouke Mauw
Abstract:
We uncover privacy vulnerabilities in the ICAO 9303 standard implemented by ePassports worldwide. These vulnerabilities, confirmed by ICAO, enable an ePassport holder who recently passed through a checkpoint to be reidentified without opening their ePassport. This paper explains how bisimilarity was used to discover these vulnerabilities, which exploit the BAC protocol - the original ICAO 9303 sta…
▽ More
We uncover privacy vulnerabilities in the ICAO 9303 standard implemented by ePassports worldwide. These vulnerabilities, confirmed by ICAO, enable an ePassport holder who recently passed through a checkpoint to be reidentified without opening their ePassport. This paper explains how bisimilarity was used to discover these vulnerabilities, which exploit the BAC protocol - the original ICAO 9303 standard ePassport authentication protocol - and remains valid for the PACE protocol, which improves on the security of BAC in the latest ICAO 9303 standards. In order to tackle such bisimilarity problems, we develop here a chain of methods for the applied $π$-calculus including a symbolic under-approximation of bisimilarity, called open bisimilarity, and a modal logic, called classical FM, for describing and certifying attacks. Evidence is provided to argue for a new scheme for specifying such unlinkability problems that more accurately reflects the capabilities of an attacker.
△ Less
Submitted 1 June, 2021; v1 submitted 17 February, 2020;
originally announced February 2020.
-
A Bisimilarity Congruence for the Applied pi-Calculus Sufficiently Coarse to Verify Privacy Properties
Authors:
Ross Horne
Abstract:
This paper is the first thorough investigation into the coarsest notion of bisimilarity for the applied pi-calculus that is a congruence relation: open barbed bisimilarity. An open variant of labelled bisimilarity (quasi-open bisimilarity), better suited to constructing bisimulations, is proven to coincide with open barbed bisimilarity. These bisimilary congruences are shown to be characterised by…
▽ More
This paper is the first thorough investigation into the coarsest notion of bisimilarity for the applied pi-calculus that is a congruence relation: open barbed bisimilarity. An open variant of labelled bisimilarity (quasi-open bisimilarity), better suited to constructing bisimulations, is proven to coincide with open barbed bisimilarity. These bisimilary congruences are shown to be characterised by an intuitionistic modal logic that can be used, for example, to describe an attack on privacy whenever a privacy property is violated. Open barbed bisimilarity provides a compositional approach to verifying cryptographic protocols, since properties proven can be reused in any context, including under input prefix. Furthermore, open barbed bisimilarity is sufficiently coarse for reasoning about security and privacy properties of cryptographic protocols; in constrast to the finer bisimilarity congruence, open bisimilarity, which cannot verify certain privacy properties.
△ Less
Submitted 6 November, 2018;
originally announced November 2018.
-
Generating Witness of Non-Bisimilarity for the pi-Calculus
Authors:
Ki Yung Ahn,
Ross Horne,
Alwen Tiu
Abstract:
In the logic programming paradigm, it is difficult to develop an elegant solution for generating distinguishing formulae that witness the failure of open-bisimilarity between two pi-calculus processes; this was unexpected because the semantics of the pi-calculus and open bisimulation have already been elegantly specified in higher-order logic programming systems. Our solution using Haskell defines…
▽ More
In the logic programming paradigm, it is difficult to develop an elegant solution for generating distinguishing formulae that witness the failure of open-bisimilarity between two pi-calculus processes; this was unexpected because the semantics of the pi-calculus and open bisimulation have already been elegantly specified in higher-order logic programming systems. Our solution using Haskell defines the formulae generation as a tree transformation from the forest of all nondeterministic bisimulation steps to a pair of distinguishing formulae. Thanks to laziness in Haskell, only the necessary paths demanded by the tree transformation function are generated. Our work demonstrates that Haskell and its libraries provide an attractive platform for symbolically analyzing equivalence properties of labeled transition systems in an environment sensitive setting.
△ Less
Submitted 30 May, 2017;
originally announced May 2017.
-
A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic
Authors:
Ki Yung Ahn,
Ross Horne,
Alwen Tiu
Abstract:
Open bisimilarity is defined for open process terms in which free variables may appear. The insight is, in order to characterise open bisimilarity, we move to the setting of intuitionistic modal logics. The intuitionistic modal logic introduced, called $\mathcal{OM}$, is such that modalities are closed under substitutions, which induces a property known as intuitionistic hereditary. Intuitionistic…
▽ More
Open bisimilarity is defined for open process terms in which free variables may appear. The insight is, in order to characterise open bisimilarity, we move to the setting of intuitionistic modal logics. The intuitionistic modal logic introduced, called $\mathcal{OM}$, is such that modalities are closed under substitutions, which induces a property known as intuitionistic hereditary. Intuitionistic hereditary reflects in logic the lazy instantiation of free variables performed when checking open bisimilarity. The soundness proof for open bisimilarity with respect to our intuitionistic modal logic is mechanised in Abella. The constructive content of the completeness proof provides an algorithm for generating distinguishing formulae, which we have implemented. We draw attention to the fact that there is a spectrum of bisimilarity congruences that can be characterised by intuitionistic modal logics.
△ Less
Submitted 9 August, 2021; v1 submitted 19 January, 2017;
originally announced January 2017.
-
De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic
Authors:
Ross Horne,
Alwen Tiu,
Bogdan Aman,
Gabriel Ciobanu
Abstract:
This paper explores the proof theory necessary for recommending an expressive but decidable first-order system, named MAV1, featuring a de Morgan dual pair of nominal quantifiers. These nominal quantifiers called `new' and `wen' are distinct from the self-dual Gabbay-Pitts and Miller-Tiu nominal quantifiers. The novelty of these nominal quantifiers is they are polarised in the sense that `new' dis…
▽ More
This paper explores the proof theory necessary for recommending an expressive but decidable first-order system, named MAV1, featuring a de Morgan dual pair of nominal quantifiers. These nominal quantifiers called `new' and `wen' are distinct from the self-dual Gabbay-Pitts and Miller-Tiu nominal quantifiers. The novelty of these nominal quantifiers is they are polarised in the sense that `new' distributes over positive operators while `wen' distributes over negative operators. This greater control of bookkee** enables private names to be modelled in processes embedded as formulae in MAV1. The technical challenge is to establish a cut elimination result, from which essential properties including the transitivity of implication follow. Since the system is defined using the calculus of structures, a generalisation of the sequent calculus, novel techniques are employed. The proof relies on an intricately designed multiset-based measure of the size of a proof, which is used to guide a normalisation technique called splitting. The presence of equivariance, which swaps successive quantifiers, induces complex inter-dependencies between nominal quantifiers, additive conjunction and multiplicative operators in the proof of splitting. Every rule is justified by an example demonstrating why the rule is necessary for soundly embedding processes and ensuring that cut elimination holds.
△ Less
Submitted 15 January, 2020; v1 submitted 18 February, 2016;
originally announced February 2016.
-
Local Type Checking for Linked Data Consumers
Authors:
Gabriel Ciobanu,
Ross Horne,
Vladimiro Sassone
Abstract:
The Web of Linked Data is the cumulation of over a decade of work by the Web standards community in their effort to make data more Web-like. We provide an introduction to the Web of Linked Data from the perspective of a Web developer that would like to build an application using Linked Data. We identify a weakness in the development stack as being a lack of domain specific scripting languages for…
▽ More
The Web of Linked Data is the cumulation of over a decade of work by the Web standards community in their effort to make data more Web-like. We provide an introduction to the Web of Linked Data from the perspective of a Web developer that would like to build an application using Linked Data. We identify a weakness in the development stack as being a lack of domain specific scripting languages for designing background processes that consume Linked Data. To address this weakness, we design a scripting language with a simple but appropriate type system. In our proposed architecture some data is consumed from sources outside of the control of the system and some data is held locally. Stronger type assumptions can be made about the local data than external data, hence our type system mixes static and dynamic ty**. Throughout, we relate our work to the W3C recommendations that drive Linked Data, so our syntax is accessible to Web developers.
△ Less
Submitted 1 August, 2013;
originally announced August 2013.
-
A Provenance Tracking Model for Data Updates
Authors:
Gabriel Ciobanu,
Ross Horne
Abstract:
For data-centric systems, provenance tracking is particularly important when the system is open and decentralised, such as the Web of Linked Data. In this paper, a concise but expressive calculus which models data updates is presented. The calculus is used to provide an operational semantics for a system where data and updates interact concurrently. The operational semantics of the calculus also t…
▽ More
For data-centric systems, provenance tracking is particularly important when the system is open and decentralised, such as the Web of Linked Data. In this paper, a concise but expressive calculus which models data updates is presented. The calculus is used to provide an operational semantics for a system where data and updates interact concurrently. The operational semantics of the calculus also tracks the provenance of data with respect to updates. This provides a new formal semantics extending provenance diagrams which takes into account the execution of processes in a concurrent setting. Moreover, a sound and complete model for the calculus based on ideals of series-parallel DAGs is provided. The notion of provenance introduced can be used as a subjective indicator of the quality of data in concurrent interacting systems.
△ Less
Submitted 22 August, 2012;
originally announced August 2012.
-
A Verified Algebra for Linked Data
Authors:
Ross Horne,
Vladimiro Sassone
Abstract:
A foundation is investigated for the application of loosely structured data on the Web. This area is often referred to as Linked Data, due to the use of URIs in data to establish links. This work focuses on emerging W3C standards which specify query languages for Linked Data. The approach is to provide an abstract syntax to capture Linked Data structures and queries, which are then internalised in…
▽ More
A foundation is investigated for the application of loosely structured data on the Web. This area is often referred to as Linked Data, due to the use of URIs in data to establish links. This work focuses on emerging W3C standards which specify query languages for Linked Data. The approach is to provide an abstract syntax to capture Linked Data structures and queries, which are then internalised in a process calculus. An operational semantics for the calculus specifies how queries, data and processes interact. A labelled transition system is shown to be sound with respect to the operational semantics. Bisimulation over the labelled transition system is used to verify an algebra over queries. The derived algebra is a contribution to the application domain. For instance, the algebra may be used to rewrite a query to optimise its distribution across a cluster of servers. The framework used to provide the operational semantics is powerful enough to model related calculi for the Web.
△ Less
Submitted 31 July, 2011;
originally announced August 2011.
