08/07/2020

Cones as a model of intuitionistic linear logic

Thomas Ehrhard

Keywords: Denotational semantics, probabilistic programming languages, linear logic

Abstract: For overcoming the limitations of probabilistic coherence spaces which do not seem to provide natural interpretations of continuous data types such as the real line, we introduced with Pagani and Tasson a model of probabilistic higher order computation based on (positive) cones, and a class of totally monotone functions that we called "stable". Then Crubillé proved that this model is a conservative extension of the earlier probabilistic coherence space model. We continue these investigations by showing that the category of cones and linear and Scott-continuous functions is a model of intuitionistic linear logic. To define the tensor product, we use the special adjoint functor theorem, and we prove that this operation is an extension of the standard tensor product of probabilistic coherence spaces. We also show that these latter are dense in cones, thus allowing to lift the main properties of the tensor product of probabilistic coherence spaces to general cones. Finally we define in the same way an exponential of cones and extend measurability to these new operations.

 0
 0
 0
 0
This is an embedded video. Talk and the respective paper are published at ICALP 2020 virtual conference. If you are one of the authors of the paper and want to manage your upload, see the question "My papertalk has been externally embedded..." in the FAQ section.

Comments

Post Comment
no comments yet
code of conduct: tbd

Similar Papers