A Computational Interpretation of Compact Closed Categories
summary
Extends a reversible isomorphism language with negative types (a backward-direction effect) and pointed fractional types (indexed GC tokens that can raise failure), gives concrete bidirectional machine semantics with direction flags and a failure state, proves termination and that forward/backward evaluations are inverses (full and partial reversibility), constructs compact closed categories for both extensions, implements interpreters and a reversible SAT solver that uses backtracking plus fresh allocation/deallocation, and ships a mechanized Agda formalization and runnable artifacts.
AI-written summary · about
chapters (5)
related talks
45mA categorical view of computational effects
20mProto-Quipper with Reversing and Control
28mTowards Light-Weight Operational Reasoning for Languages with Binders, Categorically
25mCubical Synthetic Homotopy Theory
01h 07mAn introduction to synthetic guarded domain theory with applications to probabilistic(…)
25mBig-Stop Semantics: Small-Step Semantics in a Big-Step Judgment
23mFrom Semantics to Syntax: A Type Theory for Comprehension Categories
23mImplementing a category-theoretic framework for typed abstract syntax