Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Type-Based Termination for Futures

Siva Somayyajula, Frank Pfenning

TL;DR

Type-Based Termination for Futures develops a general framework of arithmetic-refined sized types for futures-based concurrency. It introduces SAX$^\infty$, extending SAX with recursion and size refinements, and SAX$^\omega$, a finitely-deep, translatable counterpart to prove termination via a novel logical-relations argument over configurations. The approach allows infinitely deep typing derivations to be reduced to infinitely wide but finite-depth proofs, enabling a compositional termination criterion in a concurrent setting. This work advances termination guarantees for mixed inductive-coinductive programs and provides a foundation for future extensions to richer types and practical implementations in concurrent functional languages.

Abstract

In sequential functional languages, sized types enable termination checking of programs with complex patterns of recursion in the presence of mixed inductive-coinductive types. In this paper, we adapt sized types and their metatheory to the concurrent setting. We extend the semi-axiomatic sequent calculus, a subsuming paradigm for futures-based functional concurrency, and its underlying operational semantics with recursion and arithmetic refinements. The latter enables a new and highly general sized type scheme we call sized type refinements. As a widely applicable technical device, we type recursive programs with infinitely deep typing derivations that unfold all recursive calls. Then, we observe that certain such derivations can be made infinitely wide but finitely deep. The resulting trees serve as the induction target of our termination result, which we develop via a novel logical relations argument.

Type-Based Termination for Futures

TL;DR

Type-Based Termination for Futures develops a general framework of arithmetic-refined sized types for futures-based concurrency. It introduces SAX, extending SAX with recursion and size refinements, and SAX, a finitely-deep, translatable counterpart to prove termination via a novel logical-relations argument over configurations. The approach allows infinitely deep typing derivations to be reduced to infinitely wide but finite-depth proofs, enabling a compositional termination criterion in a concurrent setting. This work advances termination guarantees for mixed inductive-coinductive programs and provides a foundation for future extensions to richer types and practical implementations in concurrent functional languages.

Abstract

In sequential functional languages, sized types enable termination checking of programs with complex patterns of recursion in the presence of mixed inductive-coinductive types. In this paper, we adapt sized types and their metatheory to the concurrent setting. We extend the semi-axiomatic sequent calculus, a subsuming paradigm for futures-based functional concurrency, and its underlying operational semantics with recursion and arithmetic refinements. The latter enables a new and highly general sized type scheme we call sized type refinements. As a widely applicable technical device, we type recursive programs with infinitely deep typing derivations that unfold all recursive calls. Then, we observe that certain such derivations can be made infinitely wide but finitely deep. The resulting trees serve as the induction target of our termination result, which we develop via a novel logical relations argument.

Paper Structure

This paper contains 11 sections, 9 theorems, 33 equations, 5 figures.

Table of Contents

  1. Introduction
  2. $\text{SAX}^\infty$
  3. $\text{SAX}^\omega$
  4. Operational Semantics and Termination
  5. Related Work
  6. Sized types.
  7. Size inference.
  8. Infinite and circular proofs.
  9. Session types.
  10. $\pi$-calculi.
  11. Conclusion and Future Work

Key Result

Theorem 3.1

If $\hbox{\tabskip=0pt \halign{ $$ \quad$$\cr \tabskip=0pt \halign{ $$ \quad$$\cr D\cr} $\hbox{....}$ \cr} $\cdot;\cdot;\Gamma\vdash^{\overline{n}} P::(x:A)$}$, then $\Gamma\vdash^{\omega} P::(x:A)$.

Figures (5)

  • Figure 1: $\text{SAX}^\infty$ Typing
  • Figure 2: $\text{SAX}^\omega$ Typing Rules
  • Figure 3: Configuration Typing
  • Figure 4: Operational Semantics
  • Figure 5: Compatibility Lemmas

Theorems & Definitions (30)

  • Example 1.1: Recursive types
  • Example 1.2: Evens and odds I
  • Definition 2.1: Type
  • Definition 2.2: Process
  • Example 2.3: Evens and odds II
  • Example 2.4: Typechecking
  • Example 2.5: Naïve Quicksort
  • Example 2.6: Left-fair streams
  • Example 2.7: Stream processors
  • Theorem 3.1: Translation
  • ...and 20 more