A mixed modal/linear lambda calculus with applications to Bellantoni-Cook safe recursion

. This paper introduces a simply-typed lambda calculus with both modal and linear function types. Through the use of subtyping extra term formers associated with modality and linearity are avoided. We study the basic metatheory of this system including existence and inference of principal types. The system serves as a platform for certain higher-order generalisations of Bellantoni-Cook's function algebra capturing polynomial time using a separation of the variables into "safe" and "normal" ones. The distinction between and the syntactic restrictions involved with the safe and normal variables in the Bellantoni-Cook framework are captured by the modal function space and the associated typing rules. The linear function spaces on the other hand are used to enable a certain form of primitive recursion with functional result type which is conservative over polynomial time. The proofs associated with these applications are based on an interpretation of the lambda calculus in a category-theor..