https://j-towns.github.io/papers/flipper-short.pdf ‘Flipper’ (available at github.com/j-towns/flipper) Verified Reversible Programming for Verified Lossless Compression James Townsend and Jan-Willem van de Meent University of Amsterdam Abstract Lossless compression implementations typically contain two programs, an encoder and a decoder, which are required to be inverse to one another. We observe that a significant class of compression methods, based on asymmetric numeral systems (ANS), have shared structure between the encoder and decoder—the decoder program is the ‘reverse’ of the encoder program—allowing both to be simultaneously specified by a single, reversible function. To exploit this, we have implemented a small reversible language, embedded in Agda, which we call ‘Flipper’ (available at github.com/j-towns/flipper). Agda supports formal verification of program properties, and the compiler for our reversible language (which is implemented as an Agda macro), produces not just an encoder/decoder pair of functions but also a proof that they are inverse to one another. Thus users of the language get formal verification ‘for free’. We give a small example use-case of Flipper in this paper, and plan to publish a full compression implementation soon.