Choice trees [Chappe, et al., 2023] is a new data structure that combines coinductive trees of computations with nondeterministic branching to naturally model internal nondeterminism and concurrency. Interaction trees, a preceding similar data structure, can be embedded into choice trees by a monad morphism. Choice trees are originally implemented in the Coq (Rocq) proof assistant. The aim of this project is to implement this choice trees (and its library) in the HOL4 theorem prover.
In a broader context, this project relates to the bigger and on-going project of the Pancake programming language. 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. Pancake has a semantics based on interaction trees and we are interested in investigating possible applications of choice trees to Pancake semantics and related verification, but this is out of the scope for the current Taste of Research project.
School
Computer Science and Engineering
Research Area
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 HOL4 github repository with an implementation and HOL4 formalisation.
- N. Chappe, et al. "Choice Trees"
- Pancake Systems Language for verified OS components