Positive Focusing is Directly Useful
Abstract
Recently, Miller and Wu introduced the positive λ-calculus, a call-by-value λ-calculus with sharing obtained by assigning proof terms to the positively polarized focused proofs for minimal intuitionistic logic. The positive λ-calculus stands out among λ- 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.
Domains
Computer Science [cs]Origin | Files produced by the author(s) |
---|