Proving termination of evaluation for System F with control operators

TL;DR

This paper provides new proofs of termination for evaluation in System F with control operators, using a modified reducibility candidates approach that handles various control operators and evaluation strategies.

Contribution

It introduces a novel proof method based on reducibility candidates for System F with control operators, covering abortive and delimited controls, and both call-by-value and call-by-name strategies.

Findings

Proved termination of evaluation in System F with control operators.

Developed a modified reducibility candidates proof technique.

Addressed both callcc and shift/reset control operators.

Abstract

We present new proofs of termination of evaluation in reduction semantics (i.e., a small-step operational semantics with explicit representation of evaluation contexts) for System F with control operators. We introduce a modified version of Girard's proof method based on reducibility candidates, where the reducibility predicates are defined on values and on evaluation contexts as prescribed by the reduction semantics format. We address both abortive control operators (callcc) and delimited-control operators (shift and reset) for which we introduce novel polymorphic type systems, and we consider both the call-by-value and call-by-name evaluation strategies.