Deferring the Details and Deriving Programs

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

Abstract

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
Pages27–39
Number of pages13
ISBN (Print)9781450368155
DOIs
Publication statusPublished - 18 Aug 2019
EventWorkshop on Type-Driven Development 2019 - Berlin, Germany
Duration: 18 Aug 201918 Aug 2019
https://icfp19.sigplan.org/home/tyde-2019

Conference

ConferenceWorkshop on Type-Driven Development 2019
Abbreviated titleTyDe 2019
Country/TerritoryGermany
CityBerlin
Period18/08/1918/08/19
Internet address

Keywords

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

Fingerprint

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

Cite this