Resource approximation for the $\lambda\mu$-calculus

TL;DR

This paper develops a resource-aware approximation theory for the $mbda-calculus by adapting Taylor expansion, enabling new insights into its properties and limitations regarding parallel computations.

Contribution

It introduces a novel resource approximation framework for the $mbda-calculus based on Taylor expansion, addressing its lack of approximation notions.

Findings

Establishes a resource conscious $mbda-theory

Proves properties like Stability and Perpendicular Lines Property

Shows the impossibility of parallel computations

Abstract

The $\lambda\mu$-calculus plays a central role in the theory of programming languages as it extends the Curry-Howard correspondence to classical logic. A major drawback is that it does not satisfy B\"ohm's Theorem and it lacks the corresponding notion of approximation. On the contrary, we show that Ehrhard and Regnier's Taylor expansion can be easily adapted, thus providing a resource conscious approximation theory. This produces a sensible $\lambda\mu$-theory with which we prove some advanced properties of the $\lambda\mu$-calculus, such as Stability and Perpendicular Lines Property, from which the impossibility of parallel computations follows.