LFCS Seminar: 24 November 2020 - Amr Sabry

Title: Programming with Negative and Fractional Types  

Abstract: Computation is a physical process that obeys, among other laws, the law of conservation of information. Designing a first-order language that embraces this principle is relatively simple only requiring the well-established isomorphisms between finite types. This first-order language is reversible, has a simple operational semantics, and has a categorical semantics in bimonoidal categories. Monoidal categories have higher-order extensions called compact closed categories whose main ingredient is the presence of dual objects. In the setting of type theory, this requires a “negative type” that acts as a dual to the conventional sum type, and a “fractional type” that acts as a dual to the conventional product type. The categorical semantics of these dual objects is well-established but what could they correspond to in the world of operational semantics? The main technical results are an interpretation of negative types using backtracking, an interpretation of fractional types using garbage-collection, and an illustration of the expressive power of these type constructors for higher-order programming in a reversible language. The material is based on several publications culminating with a recent POPL 2021 paper with Ph.D. student Chao-Hong Chen.

Affiliation: Quantum Science and Engineering Center, Luddy School of Informatics, Computing, and Engineering at Indiana University Bloomington, USA.