Title: Ehrhard’s exponential modalities are free!

Abstract: Ehrhard introduced models of linear logic based on “Finiteness spaces” in 2005. Priyaa Srinivasan, Cole Comfort and I used one of these models (finiteness matrices) as a model for our version of infinite dimensional quantum mechanics. To model certain quantum phenomena, we needed free exponential modalities and set out to prove that Ehrhard’s are free … to discover (belatedly) that they are, indeed, free thanks to JS pointing us at Christine Tasson’s PhD. thesis!

The talk introduces the linear logic models based on finiteness spaces and develops what we expected to be the free exponential modalities therein (which is the E_\inft of Tasson, Tabareau, and Mellies) … but which we belatedly discovered fails to be such.