Dependent Type Refinements for Futures

TL;DR

This paper introduces dependent type refinements for SAX, a futures-based process calculus, enabling reasoning about partial correctness and data encapsulation in concurrent programs with recursion.

Contribution

It extends type refinement techniques to SAX, combining proof theory, bidirectional typing, and Hoare logic for enhanced program verification.

Findings

Proved syntactic type soundness for the system

Enabled reasoning about partial correctness of SAX programs

Demonstrated data and codata encapsulation in examples

Abstract

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.