Formalisation catégorielle des systèmes de types dépendants avec effets algébriques

Nous développons une sémantique catégorielle complète pour les langages de programmation à types dépendants intégrant des effets algébriques, en établissant la correspondance de Curry-Howard-Lambek dans ce cadre enrichi.