Extracting Agda-embedded DSLs

Artem Shinkarov


Date: Wed, January 13, 2021
Time: 12:00
Room: Jesper's Zoom Room


A lot of programming languages sacrifice safety for the sake of performance and usability. For example, C offers great performance, Python is very easy to use, but neither of the languages provide a way to verify that division by zero or out-of-bound array indexing does not occur in the given program. Extending languages with such safety guarantees tends to require very invasive changes of the tooling and/or language semantics.

In this work we explore an alternative approach. We consider a shallow embedding of the language of interest into Agda and use dependent types to encode invariants of interest. Any program that could be possibly written in such a system would automatically respect the chosen properties. We then provide a framework that makes it possible to extract embedded programs (and verified properties) back into the original language. Extraction step is written in Agda using its reflection mechanisms. Agda’s rewriting capabilities make it possible to apply formally verified program optimisations prior extraction. We demonstrate our framework in action by encoding two languages: Kaleidoskope and a subset of APL that we extract into a high-performance array language SaC.

Previous: |
Next: Cas van der Rest |