Quentin Vermande

Doctorant

Centre Inria d'Université Côte d'Azur

Contact

: qvermande [arobase] phare.normalesup.org
: Clé publique SSH

Qui suis-je ?

Je suis doctorant en première année de thèse en informatique au centre Inria d'Université Côte d'Azur, sous la direction d'Yves BERTOT et Cyril COHEN.

Je m'intéresse aux mathématiques et à l'informatique théorique, et dans ces domaines principalement à la preuve formelle.

Quelques Liens

Preuves formelles (Coq)
- Coq (en) un assistant de preuve formelle.
- Coq in a hurry (en) un court tutoriel pour Coq.
- Mathematical Components (en) la principale bibliothèque de mathématiques de Coq.
- MathComp Analysis (en) la bibliothèque d'analyse basée sur Mathematical Components.
Rationalité
- Harry Potter and the Methods of Rationality (en) une excellente fanfiction sur Harry Potter d'Eliezer Yudkowsky
- LessWrong (en) un forum dédié à l'optimisation des méthodes de raisonnement et de prise de décision.
- Effective Altruism (en) un forum dédié à l'optimisation de notre impact (positif) sur le monde.
Autres
- France-ioi (cours et problèmes) l'organisation qui organise les olympiades françaises d'informatiques. Ils proposent un excellent parcours d'apprentissage de la programmation et de l'algorithmique.
- Animath l'association française qui organise des activités mathématiques à destination des collégiens et lycéens.
- Butterick's Practical Typography (en) un livre en ligne de typographie.

Contact

Qui suis-je ?

Quelques Liens

Preuves formelles (Coq)

Rationalité

Autres