A formalisation of parameterised reference attribute grammars

Scott J.H. Buckley, Anthony M. Sloane

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionpeer-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 languageEnglish
Title of host publicationSLE 2017
Subtitle of host publicationProceedings of the 10th ACM SIGPLAN International Conference on Software Language Engineering
EditorsB Combemale, M Mernik, B Rumpe
Place of PublicationNew York, NY
PublisherAssociation for Computing Machinery, Inc
Pages139-150
Number of pages12
ISBN (Electronic)9781450355254
DOIs
Publication statusPublished - 23 Oct 2017
Event10th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2017 - Vancouver, Canada
Duration: 23 Oct 201724 Oct 2017

Conference

Conference10th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2017
CountryCanada
CityVancouver
Period23/10/1724/10/17

Keywords

  • Attribute grammars
  • Name analysis
  • Small-step operational semantics

Fingerprint Dive into the research topics of 'A formalisation of parameterised reference attribute grammars'. Together they form a unique fingerprint.

Cite this