Formalising and Verifying Reference Attribute Grammars in Coq

DOI10.1007/978-3-642-00590-9_11zbMATH Open1234.68265OpenAlexW67726583MaRDI QIDQ3617697FDOQ3617697

Authors: M. Schäfer, Torbjörn Ekman, Oege de Moor 

Publication date: 31 March 2009

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-00590-9_11

Recommendations

• Proofs of partial correctness for attribute grammars with applications to recursive procedures and logic programming
• Reference attributed grammars
• scientific article; zbMATH DE number 2090288
• Zipper-based attribute grammars and their extensions
• Remote attribute grammars

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• Coq
• Ott
• JastAdd

This page was built for publication: Formalising and Verifying Reference Attribute Grammars in Coq

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3617697)