Integration in Cones

Measurable cones, with linear and measurable functions as morphisms, are a model of intuitionistic linear logic and of probabilistic PCF which accommodates ``continuous data types'' such as the real line. So far they lacked however a major feature to make them a model of other probabilistic programming languages: a general and versatile theory of integration which is the key ingredient for interpreting the sampling programming primitives. The goal of this paper is to develop such a theory based on a notion of integrable cones and of integral preserving linear maps: our definition of integrals is an adaptation to cones of Pettis integrals in topological vector spaces. We prove that we obtain again in that way 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 the second based on a new notion of integrable analytic function on cones.