Quentin Vermande

PhD student

Inria Centre at Université Côte d'Azur

Contact

: qvermande [at] phare.normalesup.org
: SSH public key

About me

I am a first year PhD student in computer science at the Inria centre at Université Côte d'Azur, under the supervision of Yves BERTOT and Cyril COHEN.

My main interests lie in mathematics and theoretical computer science, and particularly in formal proofs.

Some links

Formal proofs (Coq)
- Coq a formal proof assistant.
- Coq in a hurry a short tutorial to get started in Coq.
- Mathematical Components Coq's main mathematics library.
- MathComp Analysis the analysis library based on Mathematical Components.
Rationality
- Harry Potter and the Methods of Rationality an excellent fanfiction for Harry Potter written by Eliezer Yudkowsky
- LessWrong a forum dedicated to optimizing reasonning and decision-making.
- Effective Altruism a forum dedicated to optimizing our (positive) impact on the world.
Misc.
- France-ioi (courses and tasks) the organization that organises the french olympiad in informatics. They provide an excellent introduction to programming and algorithmics.
- Animath (fr) the french association which organizes activities in mathematics for high school students.
- Butterick's Practical Typography a typography web-based book.

Contact

About me

Some links

Formal proofs (Coq)

Rationality

Misc.