| Summary: | <p>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.</p>
<p>The models we build are in the style of Moggi, namely, a cartesian closed category with a monad for modelling non termination. More specifically, our general method builds sheaf categories by specifying a concrete site with a class of admissible monomorphisms, a concept which we define. We combine this approach with techniques from synthetic and axiomatic domain theory to obtain a lifting monad on the sheaf category and to model recursion. We then prove the models obtained in this way are computationally adequate.</p>
|
|---|