Girard's $!()$ as a reversible fixed-point operator

TL;DR

This paper provides a categorical framework for understanding Girard's exponential as a reversible fixed-point operator within the Geometry of Interaction, highlighting its role in reversible logic and computation.

Contribution

It introduces a categorical interpretation of the exponential in Geometry of Interaction as a fixed-point operator for reversible logic, emphasizing the 'type-forgetting' aspect.

Findings

Exponential can be modeled as a fixed-point in reversible logic

Categorical description clarifies the role of 'type-forgetting' in GoI

Reversible fixed-point interpretation enhances understanding of Girard's exponential

Abstract

We give a categorical description of the treatment of the !() exponential in the Geometry of Interaction system, with particular emphasis on the fact that the GoI interpretation 'forgets types'. We demonstrate that it may be thought of as a fixed-point operation for reversible logic & computation.