Interoperability between dependently typed and non-dependently typed languages

Interoperability between dependently typed and non-dependently typed languages
Master Project

Thesis

https://resolver.tudelft.nl/uuid:0a13ca4a-9d3c-416e-bb88-affc3f14ee52

Problem statement

Dependent types are a powerful tool for ensuring the correctness of our programs. However, proving correctness of our programs is a daunting task, especially in a larger project where not every part might have a formal specification. The goal of the Agda2Hs translator is to provide a smooth integration between code written in the dependently typed language Agda and the non-dependently typed language Haskell. In particular, it makes use of erasure annotations in Agda to mark what parts of the Agda program should be removed to end up with the corresponding Haskell code.

Project description

The broad goal of this project is to investigate and improve the feasibility of implementing and verifying parts of a program in Agda and integrating it into a bigger Haskell code base. This could either take the form of implementing case studies applying Agda2Hs in a novel context, adding proofs to existing Haskell libraries, or by extending Agda2Hs itself with new features to improve its expressivity and usability.