Data refinement for Cogent

Gabriele Keller

Date: Fri, July 12, 2019
Time: 12:00
Room: Social Data Lab 0.E220

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 |
Next: |