Starting Date: June 2022
Prerequisites: Familiarity with Coq proof assistant; interest and aptitude for formal methods and mathematical modelling
Will results be assigned to University: No
The aim of this project is to formalise within the Coq proof assistant [1] the meta-theory of the recursive adaptive grammar framework [2]
Programming languages are usually specified on two levels. The first level defines a context-free grammar that specifies the syntax of the language. Usually, however, not all syntactically correct programs make sense, and so a further stage is required in which we specify a semantics, and define what it means for a syntactically correct program to be semantically meaningful. The latter stage can involve more complex definitions and analyses. For example, type systems belong in this second stage.
Recursive Adaptive Grammars (RAGs) are a framework for expressing formal grammars that define context-sensitive languages, but in a way that is designed to maintain much of the simplicity of the context-free approach. In fact, RAGs are capable of defining all Turing-complete languages. Because of this expressive power, they allow both the syntax and the semantics of a language to be defined at the same level, within a single mathematical framework.
The RAG mathematical framework was defined in Shutt’s MSc thesis [3], in pen-and-paper fashion. The objective of this project would be to formalise the definitions in the Coq proof assistant, and elaborate the proofs of the main properties and theorems of the framework. If we get far enough, we could even formulate and prove new properties of the system, or define a small programming language using RAGs within Coq and prove properties about it.
[1] https://coq.inria.fr/
[2] https://web.cs.wpi.edu/~jshutt/rags.html
[3] https://web.cs.wpi.edu/~jshutt/thesis/top.html