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

arXiv: https://arxiv.org/abs/2205.15917 · HTML: https://mlsanity.com/paper/2205.15917/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 31 May 2022.

## Built on by (most cited first, 2 of 2)

- [ωPAP Spaces: Reasoning Denotationally About Higher-Order, Recursive Probabilistic and Differentiable Programs](https://mlsanity.com/paper/2302.10636/) (2023)
- [Sample-Smooth Spaces: A Convenient Category for Differentiable Probabilistic Programming](https://mlsanity.com/paper/2609.26270/) (2026)

## Abstract (arXiv)

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.