A verified abstract machine for functional coroutines

TL;DR

This paper introduces a refined abstract machine for functional coroutines, providing a verified computational interpretation of Constant Domain logic, bridging control mechanisms with logical foundations.

Contribution

It presents a refined version of de Groote's abstract machine for functional coroutines and proves its correctness, linking it directly to Constant Domain logic.

Findings

Correctness of the refined abstract machine is formally proven.

Provides a direct computational interpretation of Constant Domain logic.

Enhances understanding of control mechanisms in functional programming.

Abstract

Functional coroutines are a restricted form of control mechanism, where each coroutine is represented with both a continuation and an environment. This restriction was originally obtained by considering a constructive version of Parigot's classical natural deduction which is sound and complete for the Constant Domain logic. In this article, we present a refinement of de Groote's abstract machine for functional coroutines and we prove its correctness. Therefore, this abstract machine also provides a direct computational interpretation of the Constant Domain logic.