Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E
			   __
			  / _`  _   /  /  o
			 /   ) __) /  /  / /  / /\/|
			(___/ (_/ (_ (_ / (__/ /   |

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                              JEUDI 4 mai, 10h30

                             -------------------
                             Pierre-Marie Pédrot
                             -------------------

                           Université de Ljubljana

            =====================================================
            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, non-termination,
non-determinism or writing operation. Through the light of a
call-by-push-value 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.