@inproceedings{3b6899029e93476c919f916d1c96bbad,
title = "Extracting the power of dependent types",
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. ",
keywords = "Agda, dependent types, embedded languages, program extraction, program verification, reflection",
author = "Artjoms {\v S}inkarovs and Jesper Cockx",
year = "2021",
doi = "10.1145/3486609.3487201",
language = "English",
series = "GPCE 2021 - Proceedings of the 20th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, co-located with SPLASH 2021",
publisher = "Association for Computing Machinery (ACM)",
pages = "83--95",
editor = "Eli Tilevich and {De Roover}, Coen",
booktitle = "GPCE 2021 - Proceedings of the 20th ACM SIGPLAN International Conference on Generative Programming",
address = "United States",
note = "20th 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 ; Conference date: 17-10-2021 Through 18-10-2021",
}