λ · remote 13 : Introduction aux types dépendant via Idris

Meetup zoom
Code accès 448118
Lien accessible après inscription

# Introduction aux types dépendant via Idris, par Valentin Robert @Ptival

Dans cette présentation, Valentin vous montrera comment les types dépendants étendent les capacités des types de données algébriques généralisés pour capturer statiquement des invariants complexes, tournant notre vérificateur de types en un vérificateur de preuves formelles.
Plutôt que de travailler sur les exemples usuels d’induction sur les entiers naturels et de listes indicées par leur longueur, je vous propose une introduction un peu plus excitante et pratique, où l’on verra comment les types dépendants nous permettent de capturer statiquement des notions syntaxiques et sémantiques comme la portée et le typage sains d’un langage de programmation fonctionnel encodé profondément dans le langage Idris, et nous interdit de commettre certaines classes de fautes dans l’évaluateur de ce langage.
Si le temps le permet, on étendra ce langage jouet à des fonctionnalités impératives et on essaiera d’écrire un petit simulateur symbolique fortement typé.

---
Meetup zoom
Code accès 448118
Lien accessible après inscription