The aim of this project is to formalise using proof assistant (such as Coq [1], Agda [4], or Isabelle [5]) 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 … full description “Formalising Recursive Adaptive Grammars using a Proof Assistant (available)”
Skip to content
Undergraduate Research Opportunities
Department of Computer Science, Royal Holloway, University of London