Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Dependent Type Refinements for Futures

Siva Somayyajula, Frank Pfenning

TL;DR

The paper addresses how to verify SAX programs using dependent refinements by introducing DRSAX, a framework that merges the semi-axiomatic sequent calculus with Hoare-style reasoning for futures-based processes. It develops a bidirectional typing system, a first-order assertion logic with uninterpreted functions, and a rich treatment of data and codata to achieve observable partial correctness alongside codata encapsulation. Key contributions include the formal definition of DRSAX, a syntactic type soundness theorem, and detailed mechanisms for phase changes, recursive reasoning, and refined data structures like lazy records and dependent functions, demonstrated through examples. The work advances verification in concurrent, futures-driven settings and lays groundwork for future extensions in abstraction, effects, and practical typechecking implementations.

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.

Dependent Type Refinements for Futures

TL;DR

The paper addresses how to verify SAX programs using dependent refinements by introducing DRSAX, a framework that merges the semi-axiomatic sequent calculus with Hoare-style reasoning for futures-based processes. It develops a bidirectional typing system, a first-order assertion logic with uninterpreted functions, and a rich treatment of data and codata to achieve observable partial correctness alongside codata encapsulation. Key contributions include the formal definition of DRSAX, a syntactic type soundness theorem, and detailed mechanisms for phase changes, recursive reasoning, and refined data structures like lazy records and dependent functions, demonstrated through examples. The work advances verification in concurrent, futures-driven settings and lays groundwork for future extensions in abstraction, effects, and practical typechecking implementations.

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.
Paper Structure (18 sections, 3 theorems, 25 equations, 6 figures)

This paper contains 18 sections, 3 theorems, 25 equations, 6 figures.

Table of Contents

  1. Introduction
  2. DRSAX: Semi-Axiomatic Type Theory Meets Hoare Logic
  3. Judgmental Structure
  4. Syntax
  5. Assertion Logic
  6. Phase Change: Subsumption and Type Annotation
  7. Cut, Snips, and Identity
  8. Labelled Sums and Lazy Records
  9. Dependent Types
  10. Recursion: Assume-Guarantee Reasoning and Recursion Invariants
  11. Summary
  12. Operational Semantics, Type Soundness, and Observable Partial Correctness
  13. Configuration Reduction and Typing
  14. Syntactic Type Soundness and Observable Partial Correctness
  15. Related Work
  16. ...and 3 more sections

Key Result

theorem 1

If $\cdot\vdash\C\div\Delta$ then either $\C$ is final or $\C\mapsto\C'$ for some $\C'$.

Figures (6)

  • Figure 1: Judgments
  • Figure 2: Syntax
  • Figure 3: Subtyping
  • Figure 4: Process Typing
  • Figure 5: Configuration Reduction
  • ...and 1 more figures

Theorems & Definitions (9)

  • proof
  • proof
  • theorem 1: Progress
  • proof
  • theorem 2: Preservation
  • proof
  • proof
  • theorem 3: Observable Satisfaction
  • proof