Pancake is a research programming language currently under development at UNSW, Chalmers University, ANU, and Gothenburg University. It comes with a compiler that is verified correct using the HOL4 theorem prover, and is built from the ground up for predictable compilation and ease of verification.
PEG (parsing expression grammar) is an expressive formalism for defining machine-oriented syntax that allows for parser generation. The current frontend, i.e., the parser for the concrete syntax, of the Pancake compiler uses the PEG as its core, but it does not leverage all of the features that PEG provides.
This project is to reimplement the Pancake parser to use more of the PEG advantages to improve the parser performance and the maintainability, possibly by improving the HOL4 PEG library.
School
Computer Science and Engineering
Research Area
Formal methods | Programming language | Compiler | Formal language
Suitable for recognition of Work Integrated Learning (industrial training)?
Yes
- Research environment
- Expected outcomes
- Supervisory team
- Reference material/links
The Trustworthy Systems (TS) Group is the pioneer in formal (mathematical) correctness and security proofs of computer systems software. Its formally verified seL4 microkernel, now backed by the seL4 Foundation, is deployed in real-world systems ranging from defence systems via medical devices, autonomous cars to critical infrastructure. The group's vision is to make verified software the standard for security- and safety-critical systems. Core to this a focus on performance as well as making software verification more scalable and less expensive.
- Report outlining the approach taken, tradeoffs considered and work done;
- Pull request to the HOL4 and/or the CakeML/Pancake github repositories with an implementation and HOL4 formalisation.
