A formalisation of parameterised reference attribute grammars

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

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

    Fingerprint

Keywords

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

Cite this

Buckley, S. J. H., & Sloane, A. M. (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 (pp. 139-150). New York, NY: Association for Computing Machinery, Inc. https://doi.org/10.1145/3136014.3136024