Positive Focusing is Directly Useful

Abstract

Recently, Miller and Wu introduced the positive $\hat{I}»$-calculus, a call-by-value $\hat{I}»$-calculus with sharing obtained by assigning proof terms to the positively polarized focused proofs for minimal intuitionistic logic. The positive $\hat{I}»$-calculus stands out among $\hat{I}»$-calculi with sharing for a compactness property related to the sharing of variables. We show that -- thanks to compactness -- the positive calculus neatly captures the core of useful sharing, a technique for the study of reasonable time cost models.

Paper for the proceedings of MFPS 2024