Measurable cones, with linear and measurable functions as morphisms, are a model of intuitionistic linear logic and of call-by-name probabilistic PCF which accommodates ``continuous data types'' such as the real line. So far however, they lacked a major feature to make them a model of more general probabilistic programming languages (notably call-by-value and call-by-push-value languages): a theory of integration for functions whose codomain is a cone, which is the key ingredient for interpreting the sampling programming primitives. The goal of this paper is to develop such a theory: our definition of integrals is an adaptation to cones of Pettis integrals in topological vector spaces. We prove that such integrable cones, with integral-preserving linear maps as morphisms, form a model of Linear Logic for which we develop two exponential comonads: the first based on a notion of stable functions introduced in earlier work and thesecond based on a new notion of integrable analytic function on cones.

翻译：可测锥体及其线性与可测函数作为态射，构成了直觉主义线性逻辑及含名调用概率型PCF（该逻辑可容纳如实数直线等“连续数据类型”）的模型。然而，迄今为止，这些结构尚缺乏一个关键特性来使其成为更通用概率编程语言（尤其是含值调用与含压栈调用语言）的模型：即针对余域为锥体的函数的积分理论，这是解释采样编程原语的核心要素。本文旨在发展该理论：我们定义的积分是将拓扑向量空间中的Pettis积分推广至锥体。我们证明，此类可积锥体（以保持积分的线性映射作为态射）构成了线性逻辑的模型，并为其构造了两个指数余单子：第一个基于早期工作中引入的稳定函数概念，第二个则基于锥体上可积解析函数的新定义。