01whole.pdf (1.1 MB)
Download file

Foundational Semantics of Dynamically Scheduled Attribute Grammar Evaluation

Download (1.1 MB)
thesis
posted on 23.11.2022, 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.

History

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

Notes

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

Awarding Institution

Macquarie University

Degree Type

Thesis PhD

Degree

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

Department, Centre or School

Department of Computing

Year of Award

2021

Principal Supervisor

Anthony Sloane

Rights

Copyright: The Author Copyright disclaimer: https://www.mq.edu.au/copyright-disclaimer

Language

English

Extent

228 pages