Artifact for Shoggoth: A formal foundation for strategic rewriting

Xueying Qin; Liam O'Connor; Rob van Glabbeek; Peter Höfner; Ohad Kammar; Michel Steuwer

doi:10.5281/zenodo.10125602

Artifact for Shoggoth: A formal foundation for strategic rewriting

Xueying Qin (Developer), Liam O'Connor (Developer), Rob van Glabbeek (Developer), Peter Höfner (Developer), Ohad Kammar (Developer), Michel Steuwer (Developer)

Research output: Non-textual form › Software

Abstract

This is the artifact for the paper Shoggoth : A Formal Foundation for Strategic Rewriting. We provide all mechanised proofs developed in Isabelle/HOL. In total we provide nine files (with .thy extension) containing our proof scripts for the denotational semantics, operational semantics, semantic equivalence, weakest precondition calculus and soundness of the weakest precondition calculus are discussed in the paper. Please refer to README.md for detail information as well as instructions for installing and executing this artifact.

Original language	English
Publisher	Zenodo
DOIs	https://doi.org/10.5281/zenodo.10125602
Publication status	Published - 14 Nov 2023

Keywords / Materials (for Non-textual outputs)

strategic rewriting
program transformation
weakest preconditions
semantics
mechanised formalisation

Access to Document

10.5281/zenodo.10125602Licence: Creative Commons: Attribution (CC-BY)

https://dl.acm.org/do/10.5281/zenodo.10125602/full/Licence: Creative Commons: Attribution (CC-BY)

1 Article

Shoggoth: A Formal Foundation for Strategic Rewriting
Qin, X., O’Connor, L., van Glabbeek, R., Höfner, P., Kammar, O. & Steuwer, M., 5 Jan 2024, In: Proceedings of the ACM on Programming Languages. 8, POPL, p. 61-89 29 p., 3.
Research output: Contribution to journal › Article › peer-review

Open Access
File

Cite this

@misc{513cce66a9204a36b368405f39236e05,

title = "Artifact for Shoggoth: A formal foundation for strategic rewriting",

abstract = "This is the artifact for the paper Shoggoth : A Formal Foundation for Strategic Rewriting. We provide all mechanised proofs developed in Isabelle/HOL. In total we provide nine files (with .thy extension) containing our proof scripts for the denotational semantics, operational semantics, semantic equivalence, weakest precondition calculus and soundness of the weakest precondition calculus are discussed in the paper. Please refer to README.md for detail information as well as instructions for installing and executing this artifact.",

keywords = "strategic rewriting, program transformation, weakest preconditions, semantics, mechanised formalisation",

author = "Xueying Qin and Liam O'Connor and {van Glabbeek}, Rob and Peter H{\"o}fner and Ohad Kammar and Michel Steuwer",

year = "2023",

month = nov,

day = "14",

doi = "10.5281/zenodo.10125602",

language = "English",

publisher = "Zenodo",

}

TY - ADVS

T1 - Artifact for Shoggoth

T2 - A formal foundation for strategic rewriting

A2 - Qin, Xueying

A2 - O'Connor, Liam

A2 - van Glabbeek, Rob

A2 - Höfner, Peter

A2 - Kammar, Ohad

A2 - Steuwer, Michel

PY - 2023/11/14

Y1 - 2023/11/14

N2 - This is the artifact for the paper Shoggoth : A Formal Foundation for Strategic Rewriting. We provide all mechanised proofs developed in Isabelle/HOL. In total we provide nine files (with .thy extension) containing our proof scripts for the denotational semantics, operational semantics, semantic equivalence, weakest precondition calculus and soundness of the weakest precondition calculus are discussed in the paper. Please refer to README.md for detail information as well as instructions for installing and executing this artifact.

AB - This is the artifact for the paper Shoggoth : A Formal Foundation for Strategic Rewriting. We provide all mechanised proofs developed in Isabelle/HOL. In total we provide nine files (with .thy extension) containing our proof scripts for the denotational semantics, operational semantics, semantic equivalence, weakest precondition calculus and soundness of the weakest precondition calculus are discussed in the paper. Please refer to README.md for detail information as well as instructions for installing and executing this artifact.

KW - strategic rewriting

KW - program transformation

KW - weakest preconditions

KW - semantics

KW - mechanised formalisation

U2 - 10.5281/zenodo.10125602

DO - 10.5281/zenodo.10125602

M3 - Software

PB - Zenodo

ER -

Artifact for Shoggoth: A formal foundation for strategic rewriting

Abstract

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Research output

Shoggoth: A Formal Foundation for Strategic Rewriting

Cite this