LINEAR LOGIC, COMONADS AND OPTIMAL REDUCTIONS
Andrea Asperti · Fundamenta Informaticae · 1995
The paper discusses, in a categorical perspective, some recent works on optimal graph reduction techniques for the λ-calculus. In particular, we relate the two “brackets” in [GAL92a] to the two operations associated with the comonad “!” of Linear Log