Data refinement for Cogent

Gabriele Keller

Cogent is a high-level functional language that reduces the cost of writing and formally verifying efficient systems code. In this talk, I’ll give a brief introduction of the language, and talk about our current work, on supporting data layout descriptions which enable customising memory layouts of Cogent algebraic datatypes. This extension allows programmers to write more code in Cogent and to integrate Cogent code with existing C programs (e.g. the Linux kernel) more seamlessly.

---

Previous: Andrey Mokhov | Build systems à la carte
Next: | NWO Veni on Composable and Safe-by-Construction Programming Language Definitions