disamb-verification

Supplementary Coq code for proofs related to semantics of disambiguation relations. Created as part of a master thesis.

Compiling the code

Requires The Coq Proof Assistant to be installed, tested on version 8.11.0. Running the file compile.sh compiles everything. Note: This project uses version 1.5.0 of the coq-std++ library. The compile.sh script should automatically clone this repository using Git and then compile that library using the make command.

Files

1. IGrammar.v contains all definitions related to Infix Expression Grammars.
2. IGrammarTheorems.v contains lemmas and theorems related to Infix Expression Grammars. This includes proofs for safety and completeness.
3. IGrammarBonusTheorems.v contains proofs that show our restrictions for safety and completeness are most general.
4. Similarly IPGrammar.v and IPGrammarTheorems.v are related to expression grammars containing Infix and Prefix productions.
5. IPPGrammar.v and IPPGrammarTheorems.v also allow Postfix productions.