Structural rules and resource control in logic and computation

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 in term 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 interpretations of substructural logics, by presenting a lambda calculus without thinning, corresponding to a variant of the relevant logic