A formalisation of parameterised reference attribute grammars

Scott J.H. Buckley; Anthony M. Sloane

doi:10.1145/3136014.3136024

A formalisation of parameterised reference attribute grammars

Scott J.H. Buckley, Anthony M. Sloane

School of Computing

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

Abstract

The similarities and differences between attribute grammar systems are obscured by their implementations. A formalism that captures the essence of such systems would allow for equivalence, correctness, and other analyses to be formally framed and proven. We present Saiga, a core language and small-step operational semantics that precisely captures the fundamental concepts of the specification and execution of parameterised reference attribute grammars. We demonstrate the utility of Saiga by a) proving a meta-theoretic property about attribute caching, and b) by specifying two attribute grammars for a realistic name analysis problem and proving that they are equivalent. The language, semantics and associated tests have been mechanised in Coq; we are currently mechanising the proofs.

Original language	English
Title of host publication	SLE 2017
Subtitle of host publication	Proceedings of the 10th ACM SIGPLAN International Conference on Software Language Engineering
Editors	B Combemale, M Mernik, B Rumpe
Place of Publication	New York, NY
Publisher	Association for Computing Machinery, Inc
Pages	139-150
Number of pages	12
ISBN (Electronic)	9781450355254
DOIs	https://doi.org/10.1145/3136014.3136024
Publication status	Published - 23 Oct 2017
Event	10th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2017 - Vancouver, Canada Duration: 23 Oct 2017 → 24 Oct 2017

Conference

Conference	10th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2017
Country/Territory	Canada
City	Vancouver
Period	23/10/17 → 24/10/17

Keywords

Attribute grammars
Name analysis
Small-step operational semantics

Access to Document

10.1145/3136014.3136024

Cite this

@inproceedings{ea36031a1be7442f9c628df35598cefd,

title = "A formalisation of parameterised reference attribute grammars",

abstract = "The similarities and differences between attribute grammar systems are obscured by their implementations. A formalism that captures the essence of such systems would allow for equivalence, correctness, and other analyses to be formally framed and proven. We present Saiga, a core language and small-step operational semantics that precisely captures the fundamental concepts of the specification and execution of parameterised reference attribute grammars. We demonstrate the utility of Saiga by a) proving a meta-theoretic property about attribute caching, and b) by specifying two attribute grammars for a realistic name analysis problem and proving that they are equivalent. The language, semantics and associated tests have been mechanised in Coq; we are currently mechanising the proofs.",

keywords = "Attribute grammars, Name analysis, Small-step operational semantics",

author = "Buckley, {Scott J.H.} and Sloane, {Anthony M.}",

year = "2017",

month = oct,

day = "23",

doi = "10.1145/3136014.3136024",

language = "English",

pages = "139--150",

editor = "B Combemale and M Mernik and B Rumpe",

booktitle = "SLE 2017",

publisher = "Association for Computing Machinery, Inc",

note = "10th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2017 ; Conference date: 23-10-2017 Through 24-10-2017",

}

Buckley, SJH & Sloane, AM 2017, A formalisation of parameterised reference attribute grammars. in B Combemale, M Mernik & B Rumpe (eds), SLE 2017: Proceedings of the 10th ACM SIGPLAN International Conference on Software Language Engineering. Association for Computing Machinery, Inc, New York, NY, pp. 139-150, 10th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2017, Vancouver, Canada, 23/10/17. https://doi.org/10.1145/3136014.3136024

A formalisation of parameterised reference attribute grammars. / Buckley, Scott J.H.; Sloane, Anthony M.
SLE 2017: Proceedings of the 10th ACM SIGPLAN International Conference on Software Language Engineering. ed. / B Combemale; M Mernik; B Rumpe. New York, NY: Association for Computing Machinery, Inc, 2017. p. 139-150.

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

TY - GEN

T1 - A formalisation of parameterised reference attribute grammars

AU - Buckley, Scott J.H.

AU - Sloane, Anthony M.

PY - 2017/10/23

Y1 - 2017/10/23

N2 - The similarities and differences between attribute grammar systems are obscured by their implementations. A formalism that captures the essence of such systems would allow for equivalence, correctness, and other analyses to be formally framed and proven. We present Saiga, a core language and small-step operational semantics that precisely captures the fundamental concepts of the specification and execution of parameterised reference attribute grammars. We demonstrate the utility of Saiga by a) proving a meta-theoretic property about attribute caching, and b) by specifying two attribute grammars for a realistic name analysis problem and proving that they are equivalent. The language, semantics and associated tests have been mechanised in Coq; we are currently mechanising the proofs.

AB - The similarities and differences between attribute grammar systems are obscured by their implementations. A formalism that captures the essence of such systems would allow for equivalence, correctness, and other analyses to be formally framed and proven. We present Saiga, a core language and small-step operational semantics that precisely captures the fundamental concepts of the specification and execution of parameterised reference attribute grammars. We demonstrate the utility of Saiga by a) proving a meta-theoretic property about attribute caching, and b) by specifying two attribute grammars for a realistic name analysis problem and proving that they are equivalent. The language, semantics and associated tests have been mechanised in Coq; we are currently mechanising the proofs.

KW - Attribute grammars

KW - Name analysis

KW - Small-step operational semantics

UR - http://www.scopus.com/inward/record.url?scp=85037067504&partnerID=8YFLogxK

U2 - 10.1145/3136014.3136024

DO - 10.1145/3136014.3136024

M3 - Conference proceeding contribution

AN - SCOPUS:85037067504

SP - 139

EP - 150

BT - SLE 2017

A2 - Combemale, B

A2 - Mernik, M

A2 - Rumpe, B

PB - Association for Computing Machinery, Inc

CY - New York, NY

T2 - 10th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2017

Y2 - 23 October 2017 through 24 October 2017

ER -

A formalisation of parameterised reference attribute grammars

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this