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 … full description “Coq Formalisation of Recursive Adaptive Grammars (available)”
Skip to content
Undergraduate Research Opportunities
Department of Computer Science, Royal Holloway, University of London