A Verified Algebra for Read-Write Linked Data
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 tha...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Journal Article |
| Language: | English |
| Published: |
2015
|
| Subjects: | |
| Online Access: | https://hdl.handle.net/10356/80958 http://hdl.handle.net/10220/39003 |
| _version_ | 1811689628973924352 |
|---|---|
| author | Horne, Ross Sassone, Vladimiro |
| author2 | School of Computer Engineering |
| author_facet | School of Computer Engineering Horne, Ross Sassone, Vladimiro |
| author_sort | Horne, Ross |
| collection | NTU |
| description | 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 defined 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. |
| first_indexed | 2024-10-01T05:51:08Z |
| format | Journal Article |
| id | ntu-10356/80958 |
| institution | Nanyang Technological University |
| language | English |
| last_indexed | 2024-10-01T05:51:08Z |
| publishDate | 2015 |
| record_format | dspace |
| spelling | ntu-10356/809582020-05-28T07:41:40Z A Verified Algebra for Read-Write Linked Data Horne, Ross Sassone, Vladimiro School of Computer Engineering Operational semantics Bisimulation Linked Data 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 defined 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. Accepted version 2015-12-08T07:54:03Z 2019-12-06T14:18:18Z 2015-12-08T07:54:03Z 2019-12-06T14:18:18Z 2014 Journal Article Horne, R., & Sassone, V. (2013). A verified algebra for read–write Linked Data. Science of Computer Programming, 89, 2-22. 0167-6423 https://hdl.handle.net/10356/80958 http://hdl.handle.net/10220/39003 10.1016/j.scico.2013.07.005 en Science of Computer Programming © 2013 Elsevier B.V. This is the author created version of a work that has been peer reviewed and accepted for publication by Science of Computer Programming, Elsevier B.V. It incorporates referee’s comments but changes resulting from the publishing process, such as copyediting, structural formatting, may not be reflected in this document. The published version is available at: [http://dx.doi.org/10.1016/j.scico.2013.07.005]. application/pdf |
| spellingShingle | Operational semantics Bisimulation Linked Data Horne, Ross Sassone, Vladimiro A Verified Algebra for Read-Write Linked Data |
| title | A Verified Algebra for Read-Write Linked Data |
| title_full | A Verified Algebra for Read-Write Linked Data |
| title_fullStr | A Verified Algebra for Read-Write Linked Data |
| title_full_unstemmed | A Verified Algebra for Read-Write Linked Data |
| title_short | A Verified Algebra for Read-Write Linked Data |
| title_sort | verified algebra for read write linked data |
| topic | Operational semantics Bisimulation Linked Data |
| url | https://hdl.handle.net/10356/80958 http://hdl.handle.net/10220/39003 |
| work_keys_str_mv | AT horneross averifiedalgebraforreadwritelinkeddata AT sassonevladimiro averifiedalgebraforreadwritelinkeddata AT horneross verifiedalgebraforreadwritelinkeddata AT sassonevladimiro verifiedalgebraforreadwritelinkeddata |