Idris 2 code for the OOPSLA 2023 paper 'Back to Direct Style: Typed and Tight'

This GitHub repository contains the formalization of the languages for our paper

Back to Direct Style: Typed and Tight.
Marius Müller, Philipp Schuster, Jonathan Immanuel Brachthäuser, Klaus Ostermann.
Accepted at OOPSLA 2023.

Build

Tested with Idris 2 version 0.5.1. To build just run

idris2 --build btdstt.ipkg