Siva Somayyajula ; Frank Pfenning - Dependent Type Refinements for Futures

entics:12286 - Electronic Notes in Theoretical Informatics and Computer Science, November 23, 2023, Volume 3 - Proceedings of MFPS XXXIX - https://doi.org/10.46298/entics.12286
Dependent Type Refinements for FuturesArticle

Authors: Siva Somayyajula ; Frank Pfenning

    Type refinements combine the compositionality of typechecking with the expressivity of program logics, offering a synergistic approach to program verification. In this paper we apply dependent type refinements to SAX, a futures-based process calculus that arises from the Curry-Howard interpretation of the intuitionistic semi-axiomatic sequent calculus and includes unrestricted recursion both at the level of types and processes. With our type refinement system, we can reason about the partial correctness of SAX programs, complementing prior work on sized type refinements that supports reasoning about termination. Our design regime synthesizes the infinitary proof theory of SAX with that of bidirectional typing and Hoare logic, deriving some standard reasoning principles for data and (co)recursion while enabling information hiding for codata. We prove syntactic type soundness, which entails a notion of partial correctness that respects codata encapsulation. We illustrate our language through a few simple examples.


    Volume: Volume 3 - Proceedings of MFPS XXXIX
    Published on: November 23, 2023
    Accepted on: October 16, 2023
    Submitted on: September 18, 2023
    Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 197 times.
    This article's PDF has been downloaded 101 times.