Direct Semantics for Declarative Disambiguation Rules in Coq
of Luka Miljak
Just like any general programming language can have a corresponding formal semantics, so too can syntax definition languages. In this project we will be looking at the semantics for declarative disambiguation of expression grammars. Declarative disambiguation rules include constructs such as associativity and priority. A direct semantics for increasing levels of complex expression grammars has already been developed by Luís Eduardo de Souza Amorim and Eelco Visser, which involves creating a filter over parse trees.
The goal of this project is to mechanize the proof of two properties of the semantics: Safety and Completeness. This mechanization will be done in the Coq proof assistant. Safety states that the underlying language does not change after applying the disambiguation. Completeness states that the resulting grammar after applying disambiguation is unambiguous.
This project involves the following steps for each level of complexity for expression grammars, starting with infix expression grammars:
- In the Coq proof assistant, implement the disambiguation semantics as designed by Luís Eduardo de Souza Amorim and Eelco Visser.
- Prove that safety holds for the semantics under certain conditions.
- Prove that completeness holds for the semantics under certain conditions.
Student: Luka Miljak
Supervisor(s): Eelco Visser, Robbert Krebbers