Recently, Miller and Wu introduced the positive $\lambda$-calculus, a call-by-value $\lambda$-calculus with sharing obtained by assigning proof terms to the positively polarized focused proofs for minimal intuitionistic logic.
The positive $\lambda$-calculus stands out among $\lambda$-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.

Comment: Paper for the proceedings of MFPS 2024

• 68N30 - Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
• 68Q55 - Semantics in the theory of computing