Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Sun 18 Aug 2019 11:50 - 12:10 at Aurora Borealis - Dependently Typed Programming Chair(s): William J. Bowman

A commonly-used technique in dependently-typed programming is to encode invariants about a data structure into its type, thus ensuring that the data structure is correct by construction. Unfortunately, this often necessitates the embedding of explicit proof terms within the data structure, which are not part of the structure conceptually, but merely supplied to ensure that the data invariants are maintained. As the complexity of the specifications in the types increases, these additional terms tend to clutter definitions, reducing readability. We introduce a technique where these proof terms can be supplied later, by constructing the data structure within a proof delay applicative functor. We apply this technique to Trip, our new language for Hoare-logic verification of imperative programs embedded in Agda, where our applicative functor is used as the basis for a verification condition generator, turning the typed holes of Agda into a method for stepwise derivation of a program from its specification in the form of a Hoare triple.

Liam is a PhD student at UNSW Australia working on Trustworthy Systems projects with Data61 at CSIRO (formerly known as NICTA). His PhD work focuses on the use of linear typed languages to provide easy-to-reason-about semantics for formal verification of operating system components. More broadly, his research interests include automated proof and reasoning, particularly in the context of dependently typed programming languages, type inference, static analysis, and concurrency.

Sun 18 Aug

tyde-2019-papers
10:50 - 12:10: TyDe 2019 - Dependently Typed Programming at Aurora Borealis
Chair(s): William J. BowmanUniversity of British Columbia
tyde-2019-papers10:50 - 11:10
Talk
Pre-print
tyde-2019-papers11:10 - 11:30
Talk
Sean InnesUniversity of Bristol, Nicolas WuImperial College London
Link to publication
tyde-2019-papers11:30 - 11:50
Talk
Liang-Ting ChenSwansea University, UK
Pre-print
tyde-2019-papers11:50 - 12:10
Talk
Link to publication