You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
32 lines
2.3 KiB
32 lines
2.3 KiB
---
|
|
key: >-
|
|
le_troll_dans_ta_machine_____une_courte_introduction_a_la_pensee_de_jean_yves_girard
|
|
title: >-
|
|
Le troll dans ta machine --- Une courte introduction à la pensée de Jean-Yves
|
|
Girard
|
|
id: hoiS7Cs5sWwXb632pLh2
|
|
format: quickie
|
|
tags:
|
|
- wtf
|
|
level: intermediate
|
|
speakers:
|
|
- guillaume_andrieu
|
|
videoId: null
|
|
presentation: null
|
|
draft: false
|
|
---
|
|
Jean-Yves Girard, le génial inventeur des indispensables [montres à moutarde](http://girard.perso.math.cnrs.fr/moutarde.pdf) (1990), est certes un joyeux trublion.
|
|
|
|
Mais avant d'en arriver à ce sommet indépassable, il a tout même publié deux-trois petites choses en chemin:
|
|
|
|
- Rust, vous connaissez? L'idée première du système de typage de Rust est la logique dite "[linéaire](http://girard.perso.math.cnrs.fr/linear.pdf)", due à Jean-Yves Girard (1987).
|
|
- Haskell, ça vous dit quelque chose? Les systèmes de typage de Haskell mais aussi Scala (et d'une certaine manière Java) sont basés sur le "[système F](https://en.wikipedia.org/wiki/System_F)" (ou lambda-calcul de second ordre), dû à... Jean-Yves Girard (1972).
|
|
- Idris, vous avez entendu parler? Le système de typage d'Idris est basé sur la théorie des types de Per Martin-Löf, dont la première version a été prouvée incorrecte par... Jean-Yves Girard, qui depuis possède un [paradoxe](https://en.wikipedia.org/wiki/System_U#Girard's_paradox) à son nom. (Girard et Martin-Löf sont par ailleurs de très bons potes et ont ferraillé sec contre les logiciens classiques dans leur prime jeunesse.)
|
|
|
|
Très méconnu mais probalement l'un des penseurs les plus influents pour l'informatique de ce début de XXIe siècle, Girard est tout aussi sérieux que fantasque. Son style toujours acéré et polémique s'appuie sur une vision très claire de ce que devrait être la logique: vivante, joyeuse, fertile.
|
|
|
|
Dans cette courte présentation, on s'attachera à comprendre pourquoi Girard est aussi virulent dans son discours, quels sont les objectifs de sa pensée, et pourquoi elle a déjà porté tant de fruits dans le monde de l'informatique.
|
|
|
|
----
|
|
|
|
Dans le cas d'un créneau à 40min, on pourrait donner quelques pointeurs sur ses travaux plus récents, et expliciter en quoi ils sont porteurs de nouvelles avancées pour les prochaines décennies (réseaux de démonstrations, géométrique de l'intéraction, etc.).
|
|
|