Concrete categories and higher-order recursion (With applications including probability, differentiability, and full abstraction)

TL;DR

This paper develops a unified sheaf-theoretic framework for modeling higher-order recursive programming languages, encompassing probabilistic, differentiable, and fully abstract models, with a focus on synthetic domain theory.

Contribution

It introduces a general construction of sheaf models for recursive higher-order languages using synthetic domain theory, unifying various existing models.

Findings

Constructs a family of sheaf models parametrized by concrete sites and monomorphisms.

Proves a general computational adequacy theorem for these models.

Enables modeling of probabilistic, differentiable, and fully abstract programming languages.

Abstract

We study concrete sheaf models for a call-by-value higher-order language with recursion. Our family of sheaf models is a generalization of many examples from the literature, such as models for probabilistic and differentiable programming, and fully abstract logical relations models. We treat recursion in the spirit of synthetic domain theory. We provide a general construction of a lifting monad starting from a class of admissible monomorphisms in the site of the sheaf category. In this way, we obtain a family of models parametrized by a concrete site and a class of monomorphisms, for which we prove a general computational adequacy theorem.