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 OctDisplayed time zone: Tijuana, Baja California change
10:30 - 12:00
GrammarsSLE at Regency B
Chair(s): Bernhard Rumpe RWTH Aachen University, Germany
|A Formalisation of Parameterised Reference Attribute Grammars|
Scott Buckley Macquarie University, Australia, Anthony Sloane Macquarie UniversityDOI
|Concurrent Circular Reference Attribute Grammars|
Jesper Oqvist Lund University, Görel HedinDOI
|Ensuring Non-interference of Composable Language Extensions|
Ted Kaminski University of Minnesota, Eric Van Wyk University of Minnesota, USADOI
|A Domain-Specific Controlled English Language for Automated Regulatory ComplianceIndustrial Paper|
Suman Roychoudhury Tata Consultancy Services Research, Sagar Sunkle Tata Consultancy Services Research, Deepali Kholkar Tata Consultancy Services Research, Vinay Kulkarni Tata Consultancy Services ResearchDOI