Extracting the power of dependent types

Artjoms Šinkarovs, Jesper Cockx

Research output: Chapter in Book/Conference proceedings/Edited volumeConference contributionScientificpeer-review

43 Downloads (Pure)

Abstract

Most existing programming languages provide little support to formally state and prove properties about programs. Adding such capabilities is far from trivial, as it requires significant re-engineering of the existing compilers and tools. This paper proposes a novel technique to write correct-by-construction programs in languages without built-in verification capabilities, while maintaining the ability to use existing tools. This is achieved in three steps. Firstly, we give a shallow embedding of the language (or a subset) into a dependently typed language. Secondly, we write a program in that embedding, and we use dependent types to guarantee correctness properties of interest within the embedding. Thirdly, we extract a program written in the original language, so it can be used with existing compilers and tools. Our main insight is that it is possible to express all three steps in a single language that supports both dependent types and reflection. Essentially, this allows us to express a program, its formal properties, and a compiler for it hand-in-hand, offering a lot of flexibility to programmers. We demonstrate this three-step approach by embedding a subset of the PostScript language in Agda, and illustrating it with several short examples. Thus we use the power of reflection to bring the benefits of dependent types to languages that had to go without them so far.

Original languageEnglish
Title of host publicationGPCE 2021 - Proceedings of the 20th ACM SIGPLAN International Conference on Generative Programming
Subtitle of host publicationConcepts and Experiences, co-located with SPLASH 2021
EditorsEli Tilevich, Coen De Roover
PublisherAssociation for Computing Machinery (ACM)
Pages83-95
Number of pages13
ISBN (Electronic)978-1-4503-9112-2
DOIs
Publication statusPublished - 2021
Event20th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, GPCE 2021, co-located with the ACM SIGPLAN conference on Systems, Programming, Languages, and Applications: Software for Humanity, SPLASH 2021 - Virtual, Online, United States
Duration: 17 Oct 202118 Oct 2021

Publication series

NameGPCE 2021 - Proceedings of the 20th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, co-located with SPLASH 2021

Conference

Conference20th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, GPCE 2021, co-located with the ACM SIGPLAN conference on Systems, Programming, Languages, and Applications: Software for Humanity, SPLASH 2021
Country/TerritoryUnited States
CityVirtual, Online
Period17/10/2118/10/21

Keywords

  • Agda
  • dependent types
  • embedded languages
  • program extraction
  • program verification
  • reflection

Fingerprint

Dive into the research topics of 'Extracting the power of dependent types'. Together they form a unique fingerprint.

Cite this