ICFP 2022
Sun 11 - Fri 16 September 2022 Ljubljana, Slovenia
Fri 16 Sep 2022 12:00 - 12:30 at Kosovel - Compiler and Extensions Chair(s): Marco Vassena

Modern dependently typed languages such as Agda can be used to statically enforce the correctness of programs. However, they still lack the large ecosystem of a more popular language like Haskell. To combine the strength of both approaches, we present agda2hs, a tool that translates an expressive subset of Agda to readable Haskell, erasing dependent types and proofs in the process. Thanks to Agda’s support for erasure annotations, this process is both safe and transparent to the user. Compared to other tools for program extraction, agda2hs uses a syntax that is already familiar to functional programmers, allows for both intrinsic and extrinsic approaches to verification, and produces Haskell code that is easy to read and audit by programmers with no knowledge of Agda.

We present a practical use case of agda2hs at IOG to verify properties of a program generator. While both agda2hs and its ecosystem are still young, our experiences so far show that this is a viable approach to make verified functional programming available to a broader audience.

This paper is a literate Agda script, hence all rendered (Agda) code has been typechecked.

slides (main.pdf)614KiB

Fri 16 Sep

Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change

11:00 - 12:30
Compiler and ExtensionsHaskell at Kosovel
Chair(s): Marco Vassena Utrecht University
Investigating Magic Numbers: Improving the Inlining Heuristic in the Glasgow Haskell Compiler
Celeste Hollenbeck University of Edinburgh, Michael F. P. O'Boyle University of Edinburgh, Michel Steuwer University of Edinburgh
Partial Type Constructors in Practice
Apoorv Ingle University of Iowa, Alex Hubers The University of Iowa, J. Garrett Morris The University of Iowa
Reasonable Agda is Correct Haskell: Writing Verified Haskell using agda2hs
Jesper Cockx TU Delft, Lucas Escot TU Delft, Orestis Melkonian University of Edinburgh, James Chapman Input Output, Ulf Norell Gothenburg University
Pre-print File Attached