Structural rules and resource control in logic and computation

Abstract

Control of resources and awareness of their usage has an important role in logic and lambda calculus as well as in programming languages, compiler design and program synthesis. Already Gentzen had the idea to control the use of formulae in structural rules of the sequent calculus, whereas the idea to control the use of variables interm calculi goes back to Church’s λI-calculus. This work provides an overview of the most important work in the field of resource control and presents the authors’ contributions in this field. The journey starts with the Resource control lambda calculus, continues with its sequent counterpart, the Resource control sequent lambda calculus, and concludes with computational inter-pretations of substructural logics, by presenting a lambda calculus without thinning, corresponding to a variant of the relevant logic.