Jesper Cockx | Building Agda, a language for reliable and trustworthy programs

In today's world it is more important than ever to build software that is reliable and trustworthy, especially for safety- or security-critical applications. Yet as already noted by the Dutch computer scientist Edsger Dijkstra in 1969, program testing can only show the presence of bugs, not their absence. Programming languages based on dependent types provide a strong answer to this problem: they allow programmers to state the expected properties of a program, and the computer checks that these properties are satisfied before the program is ever executed. Yet at the moment these languages require a high degree of expertise to use, and are thus inaccessible to the average programmer.

The overall goal of my research is to improve the reliability and practical usability of dependently typed languages. My main research vehicle for this is Agda, a dependently typed programming language and proof assistant developed originally in Sweden and used widely in programming languages research and beyond. In this talk, I will give an overview of three of my ongoing research lines:

1. Agda Core: A small but trustworthy core language for Agda that can be used to independently check the correctness of Agda programs.
2. Agda2Hs: A tool that enables Haskell developers to write and formally verify parts of their Haskell code in Agda.
3. User-extensible conversion checking: A collection of extensions to Agda that enable users to extend its notion of equality, including rewrite rules and proof irrelevance.