Arnaud Bailly explore le Type-Driven Development à travers des exemples en Elm, Haskell et Idris, couvrant les types algébriques, type classes, type families, etc. jusqu'aux frontières des types dépendants.
Didier Plaindoux passe de la théorie vers la pratique en examinant les définitions formelles. Les sujets incluent les types fonctions dépendants, les paires dépendantes, les types somme et l'égalité propositionnelle.
Voir sur Mobilizon →