Macquarie University
01whole.pdf (1.1 MB)
Download file

Foundational Semantics of Dynamically Scheduled Attribute Grammar Evaluation

Download (1.1 MB)
posted on 2022-11-23, 22:54 authored by Scott Buckley

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 evaluation of dynamically scheduled attribute grammars. We also present and discuss evaluation semantics for reference, parameterised, cached, and higher order attribute grammars. Saiga’s utility is demonstrated through proofs about the system’s operation, equivalence proofs between distinct Saiga attribute grammar programs, and “step count” comparisons between such programs. The language, semantics and proofs have been mechanised in Lean.


Table of Contents

1. Introduction -- 2. Background -- 3. Saiga -- 4. Saiga Extended -- 5. Higher Order Saiga -- 6. Metatheoretic Properties -- 7. Example -- 8. Mechanisation -- 9. Conclusion -- Appendix -- References


A thesis submitted to Macquarie University for the degree of Doctor of Philosophy

Awarding Institution

Macquarie University

Degree Type

Thesis PhD


Thesis (PhD), Macquarie University, Faculty of Science and Engineering, Department of Computing, 2021

Department, Centre or School

Department of Computing

Year of Award


Principal Supervisor

Anthony Sloane


Copyright: The Author Copyright disclaimer:




228 pages

Usage metrics

    Macquarie University Theses