Skip to content

Undergraduate Research Opportunities

Department of Computer Science, Royal Holloway, University of London

Undergraduate Research Opportunities

Tag: Agda

Formalising Recursive Adaptive Grammars using a Proof Assistant (available)

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)”

Author Reuben RoweCategories Programming Languages, Software Engineering, VerificationTags Agda, computer science theory, Coq, formal grammar, formalisation, Isabelle, proof assistant

Information

  • What is UROP?
  • How to Apply
  • Available projects
  • Ongoing projects
  • Completed projects

Research Areas

  • Algorithms
  • Artificial Intelligence
  • Bioinformatics
  • Blockchain Technologies
  • Compliance and Auditing
  • Cryptography
  • Cyber-Physical Systems
  • Data Science
  • Distributed Systems
  • Logic
  • Low Level Programming (Firmware)
  • Machine Learning
  • Physics
  • Programming Languages
  • Quantum Computing
  • Security Behaviours
  • Software Engineering
  • System Forensics
  • Systems Security
  • Uncategorized
  • User and Data Privacy
  • Verification

For Supervisors

  • Instructions
  • Manage Projects
Undergraduate Research Opportunities Proudly powered by WordPress