Sparcl: A Language for Partially-Invertible Computation
summary
A new language, SPARCL, implements partially-invertible computation with linear types and proves that composing such pieces yields correct invertibility where promised; it exposes invertible types to separate data that must be handled reversibly and supplies a pin operator to let dynamic values be used in static (invertible) positions. Examples reimplement list difference (subs/go) and Huffman coding, provide forward/backward functions that form bijections, and the paper gives a formal type system and bijectivity proof.
AI-written summary · about
chapters (10)
- 0:00Start
- 2:29Running Example Differences of adjacent elements in a list
- 3:14Unidirectional Implementation subs :: [Int] - [Int]
- 3:56Observations
- 5:28Our Approach: SPARCL (1/2)
- 7:20Handling Ar-typed Values in SPARCL
- 9:25subs in SPARCL
- 12:03Our Paper Includes ...
- 12:48Related Work
- 13:53Conclusion
related talks
14mVerification of Algorithm and Code Generation for Signal Transforms
27mPartial Evaluation of Reversible Flowchart Programs
06mVerified Reversible Programming for Verified Lossless Compression- 14mVerification of Algorithm and Code Generation for Signal Transforms
24mA Computational Interpretation of Compact Closed Categories
33mIntrinsically-Typed Definitional Interpreters à la Carte
45mInvertible Programs
25mA Lazy, Concurrent Convertibility Checker