Rencontre, May 11, 2017
La rencontre se tiendra en amphi B, 3ème étage, site Monod de l'ENS de Lyon.
Programme
 10:30 – 12:00

Paul Blain Levy (University of Birmingham)Invited talk: Contextual isomorphisms
What is the right notion of "isomorphism" between types, in a simple type theory? The traditional answer is: a pair of terms that are inverse, up to a specified congruence. We firstly argue that, in the presence of effects, this answer is too liberal and needs to be restricted, using Fuehrmann's notion of thunkability in the case of value types (as in callbyvalue), or using MunchMaccagnoni's notion of linearity in the case of computation types (as in callbyname). Yet that leaves us with different notions of isomorphism for different kinds of type.
This situation is resolved by means of a new notion of ``contextual'' isomorphism (or morphism), analogous at the level of types to contextual equivalence of terms. A contextual morphism is a way of replacing one type with the other wherever it may occur in a judgement, in a way that is preserved by the action of any term with holes. For types of pure $\lambda$calculus, we show that a contextual morphism corresponds to a traditional isomorphism. For value types, a contextual morphism corresponds to a thunkable isomorphism, and for computation types, to a linear isomorphism.
The results are most easily formulated in the setting of callbypushvalue, which we briefly introduce during the talk. This is a finegrained effectful calculus that subsumes callbyvalue and callbyname and distinguishes values from computations and value types from computation types.
 14:00 – 15:00

PierreMarie Pédrot (University of Ljubljana)Invited talk: An Effectful Way to Eliminate Addiction to Dependence
We define a syntactic monadic translation of type theory, called the weaning translation, that allows for a large range of effects in dependent type theory, such as exceptions, nontermination, nondeterminism or writing operation. Through the light of a callbypushvalue decomposition, we explain why the traditional approach fails with type dependency and justify our approach. Crucially, the construction requires that the universe of algebras of the monad forms itself an algebra. The weaning translation applies to a version of the Calculus of Inductive Constructions with a restricted version of dependent elimination, dubbed Baclofen Type Theory, which we conjecture is the proper generic way to mix effects and dependence. This provides the first effectful version of CIC, which can be implemented as a Coq plugin.
 15:30 – 16:30

Christine Tasson (IRIF, Univ. Paris Diderot)Invited talk: Probabilistic Call by Push Value
We introduce a probabilistic extension of Levy’s CallByPushValue. This extension consists simply in adding a “flipping coin” boolean closed atomic expression. This language can be understood as a major generalization of Scott’s PCF encompassing both callbyname and callbyvalue and featuring recursive (possibly lazy) data types. We interpret the language in the previously introduced denotational model of probabilistic coherence spaces, a categorical model of full classical Linear Logic, interpreting data types as coalgebras for the resource comonad. We prove adequacy and full abstraction, generalizing earlier results to a much more realistic and powerful programming language.
This is joint work with Thomas Ehrhard.