Théorie des types et réalisabilité

Date et lieu : le mercredi à 14h, salle 1007, Sophie Germain

Responsable : Hugo Herbelin et Paul-André Melliès

  • Jeudi 16 mars 2017, 14h : Pierre-Marie Pédrot, 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.

  • Mercredi 14 octobre 2015 : Danko Ilik, The exp-log normal form of formulas
  • Mercredi 16 septembre 2015 :
    • à 14h : Alexandre Miquel, An axiomatic presentation of forcing (or: forcing for the dummies)
    • à 15h : Nicolas Tabareau, Vers un analogue de l'axiome de Giraud en HoTT
  • Mercredi 9 septembre 2015 : Andrej Bauer, A sound and complete language for type theory with equality reflection