Computer Science and Engineering
Low-level systems programming such as device driver development is tedious and error-prone. Pancake is a research programming language currently under development at Chalmers University of Technology, KTH, 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 semantics of Pancake is currently formalised as functional big-step semantics, which is convenient for compiler correctness proofs. Unfortunately, this style of semantics is awkward for verification of interactive programs such as device drivers, because it requires a fully deterministic model of the device.
The aim of this project is to develop a denotational semantics for Pancake, where the meaning of programs are represented by interactive trees. Interaction trees are a new general-purpose coinductive data structures that describes environment interactions in a branching-time style. This new semantics should be defined in the HOL4 interactive theorem prover, and proven sound and complete wrt. the existing semantics.
School
Research Area
Operating systems and programming languages
- 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.
- Pull request against the CakeML repository with definitions and proofs.
- Report outlining the work undertaken.
