Modular Termination for Second-Order Computation Rules and Application to Algebraic Effect Handlers

TL;DR

This paper introduces a modular proof method for termination in second-order computation, implemented in the SOL tool, and applies it to algebraic effect handlers in higher-order calculi.

Contribution

It presents a new modular termination proof technique for second-order calculi, utilizing semantic labelling and the General Schema, with an implementation in SOL.

Findings

Successfully proved termination of a call-by-push-value calculus variant with algebraic effects.

Demonstrated SOL's effectiveness in solving higher-order termination problems.

Provided a modular approach adaptable to various higher-order calculi.

Abstract

We present a new modular proof method of termination for second-order computation, and report its implementation SOL. The proof method is useful for proving termination of higher-order foundational calculi. To establish the method, we use a variation of semantic labelling translation and Blanqui's General Schema: a syntactic criterion of strong normalisation. As an application, we apply this method to show termination of a variant of call-by-push-value calculus with algebraic effects and effect handlers. We also show that our tool SOL is effective to solve higher-order termination problems.