Verifying Five Haskell Libraries with Agda2Hs

Jesper Cockx


Date: Wed, June 02, 2021
Time: 12:00
Room: Jesper's Zoom Room


Agda2Hs https://github.com/agda/agda2hs is a new backend for Agda that translates a subset of Agda to readable Haskell code. The main goal of this project is to write and verify code in Agda that can be integrated seamlessly into Haskell projects. In this talk I will report on the work done by five undergraduate students at TU Delft to port five Haskell libraries (Data.Map and Data.Sequence from the containers package, Data.Graph.Inductive from the fgl package, and the QuadTree and Ranged-sets packages) to Agda, verify their pre- and post-conditions and internal invariants, and translate the verified implementations back to Haskell using Agda2Hs.

Previous: Phil Misteli |
Next: |