A Formalisation of Parameterised Reference Attribute Grammars
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.
Tue 24 Oct
|10:30 - 10:55|
|10:55 - 11:20|
|11:20 - 11:45|
|11:45 - 12:00|
Suman RoychoudhuryTata Consultancy Services Research, Sagar SunkleTata Consultancy Services Research, Deepali KholkarTata Consultancy Services Research, Vinay KulkarniTata Consultancy Services ResearchDOI