Deferring the Details and Deriving Programs

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publicationProceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven Development
Place of PublicationNew York, NY, USA
PublisherACM Association for Computing Machinery
Number of pages13
ISBN (Print)9781450368155
Publication statusPublished - 18 Aug 2019
EventWorkshop on Type-Driven Development 2019 - Berlin, Germany
Duration: 18 Aug 201918 Aug 2019


ConferenceWorkshop on Type-Driven Development 2019
Abbreviated titleTyDe 2019
Internet address


  • agda
  • types
  • applicative functor
  • verification conditions
  • imperative programming
  • hoare logic


Dive into the research topics of 'Deferring the Details and Deriving Programs'. Together they form a unique fingerprint.

Cite this