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 Times are displayed in time zone: Tijuana, Baja California change
10:30 - 12:00
|A Formalisation of Parameterised Reference Attribute Grammars|
|Concurrent Circular Reference Attribute Grammars|
|Ensuring Non-interference of Composable Language Extensions|
|A Domain-Specific Controlled English Language for Automated Regulatory ComplianceIndustrial Paper|
Suman RoychoudhuryTata Consultancy Services Research, Sagar SunkleTata Consultancy Services Research, Deepali KholkarTata Consultancy Services Research, Vinay KulkarniTata Consultancy Services ResearchDOI