Description of field of research:

Cogent is a linearly-typed functional programming language implemented in Haskell for writing trustworthy and efficient systems code. It has a certifying compiler that produces C code, a shallow embedding in the Isabelle/HOL theorem prover, and an Isabelle/HOL proof that the C code refines the shallow embedding. Cogent's linear type system ensures desired properties such as memory-safety (e.g. no buffer-overflows and no null pointer exceptions) and it also allows the compiler to generate efficient C code.

We are currently adding a limited form of arrays to Cogent. In order to maintain our memory-safety guarantees, we need to ensure that arrays are accessed properly and that array indices are always within the array bounds. In order to establish this, we plan to extend the Cogent type-system to support refinement types. Refinement types allow limiting classic types to ones that satisfy certain propositions. An expression is well-typed in a refinement type system if it is well-typed in the underlying type-system and if it satisfies all the propositions specified in the types. We currently have a preliminary implementation of refinement types in Cogent.

Research Area

Programming Languages and Formal Methods

This project is in collaboration with the Trustworthy Systems group. They are world leaders in research and engineering for providing unprecedented security, safety, reliability and efficiency for software systems. Successes include deployment of the OKL4 microkernel in billions of devices, the first formally verified OS kernel, seL4, and a complete seL4-based high-assurance system successfully embedded in an autonomous helicopter from Boeing. You will work with a unique combination of programming language, OS and formal methods experts, producing high-impact work with real-world applicability, driven by ambition and team spirit.

Outcome: The aim of this project is to extend the Cogent compiler to support refinement types and demonstrate the extension on a number of Cogent programs that use array and refinement types. Namely, you will extend the type-checker and if time allows you will also extend the Isabelle/HOL formalization.

Novelty: This work will enrich Cogent's linear type-system with refinement types. In the process it will involve investigating how to combine the guarantees provided by these two type-systems into an overall compiler-generated guarantee that well-typed Cogent programs are memory-safe.