Computer Science and Engineering
Pancake is a research programming language currently under development at Chalmers University of Technology, ANU, and UNSW. It comes with a formally verified compiler and is built from the ground up for predictable compilation and ease of verification.
The compiler is an optimising compiler going throgh many passes and intermediate languages, but there is scope to add many more to improve the quality and performance of generated code. Example improvements we're looking for include:
- Adding loops to the CakeML intermediate languages, to avoid the Pancake compiler having to perform tail recursion introduction to compile loops.
- Adding support for string literals to the language.
- Better instruction targeting.
These are just examples; the precise contents of this topic needs to be negotiated with the supervisors.
School
Research Area
Operating systems | Programming languages | Formal methods
- 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 CakeML/Pancake github repository with an implementation and HOL4 formalisation.
