This paper was guest-edited by Harry Mairson and Bruce Kapron, for our intended Special Issue on Functional Programming and Computational Complexity. Other papers submitted for the special issue were either out-of-scope or otherwise unsuitable for JFP. Even though only one paper met their high standards, this did not make Harry and Bruce's job any easier, and we thank them for their efforts.

In previous work the author has introduced a lambda calculus SLR with modal and linear types which serves as an extension of Bellantoni–Cook's function algebra BC to higher types. It is a step towards a functional programming language in which all programs run in polynomial time. While this previous work was concerned with the syntactic metatheory of SLR in this paper we develop a semantics of SLR in terms of Chu spaces over a certain category of sheaves from which it follows that all expressible functions are indeed in PTIME. We notice a similarity between the Chu space interpretation and CPS translation which as we hope will have further applications in functional programming.