A Computational Interpretation of Compact Closed Categories: Reversible Programming with Negative and Fractional Types
Compact closed categories include objects representing higher-order functions and are well-established as models of linear logic, concurrency, and quantum computing. We show that it is possible to construct such compact closed categories for conventional sum and product types by defining a dual to sum types, a negative type, and a dual to product types, a fractional type. Inspired by the categorical semantics, we define a sound operational semantics for negative and fractional types in which a negative type represents a computational effect that “reverses execution flow” and a fractional type represents a computational effect that “garbage collects” values or throws exceptions.
Specifically, we extend a first-order reversible language of type isomorphisms with negative and fractional types, specify an operational semantics for each extension, and prove that each extension forms a compact closed category. We furthermore show that both operational semantics can be merged using the standard combination of backtracking and exceptions resulting in a smooth interoperability of negative and fractional types. We illustrate the expressiveness of this combination by writing a reversible SAT solver that uses backtracking search along freshly allocated and de-allocated locations. The operational semantics, most of its meta-theoretic properties, and all examples are formalized in a supplementary Agda package.
Wed 20 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:00
|A Computational Interpretation of Compact Closed Categories: Reversible Programming with Negative and Fractional Types
POPLLink to publication DOI
|Internalizing Representation Independence with Univalence
Carlo Angiuli Carnegie Mellon University, Evan Cavallo Carnegie Mellon University, Anders Mörtberg Department of Mathematics, Stockholm University, Max Zeuner Stockholm UniversityLink to publication DOI
|Petr4: Formal Foundations for P4 Data Planes
Ryan Doenges Cornell University, Mina Tahmasbi Arashloo Cornell University, Santiago Bautista Univ Rennes, ENS Rennes, Inria, IRISA, Alexander Chang Cornell University, Newton Ni Cornell University, Samwise Parkinson Cornell University, Rudy Peterson Cornell University, Alaia Solko-Breslin Cornell University, Amanda Xu Cornell University, Nate Foster Cornell UniversityLink to publication DOI Pre-print
|The (In)Efficiency of Interaction
Beniamino Accattoli Inria & Ecole Polytechnique, Ugo Dal Lago University of Bologna, Italy / Inria, France, Gabriele Vanoni University of Bologna & INRIA Sophia AntipolisLink to publication DOI
|Functorial Semantics for Partial Theories
Chad Nester Tallinn University of Technology, Ivan Di Liberti Czech Academy of Sciences, Fosco Loregian Tallinn University of Technology, Pawel Sobocinski Tallinn University of TechnologyLink to publication DOI