Verified Reversible Programming for Verified Lossless Compression
summary
A tiny reversible language called Flipper is implemented as an Agda macro that compiles a single reversible codec function into an encoder, a decoder and machine-checked proofs that they are mutual inverses. It targets ANS-style lossless codecs by exploiting encoder/decoder symmetry, demonstrates a reversible pair-swap example, and reports a working but unfinished compression pipeline (I/O glue and packaging pending). Current rough edges: termination checker annotations are sometimes required and some bookkeeping still needs completion.
AI-written summary · about
related talks
27mPartial Evaluation of Reversible Flowchart Programs
15mSparcl: A Language for Partially-Invertible Computation
18mA Verified Compiler for a Functional Tensor Language
18mDeferring the Details and Deriving Programs
22mSymmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible
25mA Lazy, Concurrent Convertibility Checker
01h 05mAll the Languages Together
24mA Computational Interpretation of Compact Closed Categories