Concrete sheaf models of higher-order recursion - Matache, C (2022)
This thesis studies denotational models, in the form of sheaf categories, of functional programming languages with higher-order functions and recursion. We give a general method for building such models and show how the method includes examples such as existing models of probabilistic and differentiable computation. Using our method, we build a new fully abstract sheaf model of higher-order recursion inspired by the fully abstract logical relations models of O’Hearn and Riecke. In this way, we show that our method for building sheaf models can be used both to unify existing models that have so far been studied separately and to discover new models.