A verified algebra for read-write Linked Data

Ross Horne*, Vladimiro Sassone

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

5 Citations (Scopus)


The aim of this work is to verify an algebra for high level languages for reading and writing Linked Data. Linked Data is raw data published on the Web and interlinked using a collection of standards. The main innovation is simply to use dereferenceable URIs as global identifiers in data, rather than a key local to a dataset. This introduces significant challenges for managing data that is pulled from distributed sources over the Web. An algebra is an essential contribution to this application domain, for rewriting programs that read and write Linked Data. To verify the algebra, a syntax, operational semantics and proof technique are introduced. The syntax provides an abstract representation for a high level language that concisely captures queries and updates over Linked Data. The behaviour of the language is deined using a concise operational semantics. The natural notion of behavioural equivalence, contextual equivalence, is shown to coincide with the bisimulation proof technique. Bisimulation is used to verify that the algebra preserves the operational semantics, hence rewrites of programs using the algebra do not change their operational meaning. A novel combination of techniques is used to establish the correctness of the proof technique itself.

Original languageEnglish
Pages (from-to)2-22
Number of pages21
JournalScience of Computer Programming
Issue numberPart A
Early online date24 Jul 2013
Publication statusPublished - 1 Sept 2014


  • bisimulation
  • Linked Data
  • operational semantics


Dive into the research topics of 'A verified algebra for read-write Linked Data'. Together they form a unique fingerprint.

Cite this