On stratified regions

TL;DR

This paper proves that a stratified type and effect system guarantees termination of well-typed programs in a multi-threaded lambda-calculus with various scheduling and interaction features, using reducibility candidates.

Contribution

It introduces a proof technique based on reducibility candidates to show termination for a complex, multi-threaded lambda-calculus with stratified type and effect systems.

Findings

Stratification ensures termination of typable programs.

The proof applies to a multi-threaded lambda-calculus with diverse scheduling.

The approach covers references, channels, and signals.

Abstract

Type and effect systems are a tool to analyse statically the behaviour of programs with effects. We present a proof based on the so called reducibility candidates that a suitable stratification of the type and effect system entails the termination of the typable programs. The proof technique covers a simply typed, multi-threaded, call-by-value lambda-calculus, equipped with a variety of scheduling (preemptive, cooperative) and interaction mechanisms (references, channels, signals).