Beniamino Accattoli ; Jui-Hsuan Wu - Positive Focusing is Directly Useful

entics:14758 - Electronic Notes in Theoretical Informatics and Computer Science, December 11, 2024, Volume 4 - Proceedings of MFPS XL - https://doi.org/10.46298/entics.14758
Positive Focusing is Directly UsefulArticle

Authors: Beniamino Accattoli ; Jui-Hsuan Wu

    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.


    Volume: Volume 4 - Proceedings of MFPS XL
    Published on: December 11, 2024
    Accepted on: November 18, 2024
    Submitted on: November 15, 2024
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages

    Consultation statistics

    This page has been seen 22 times.
    This article's PDF has been downloaded 9 times.