Pierre-yves Strub (史都伯)

me

Non-permanent researcher at INRIA / Microsoft Joint Center
Secure Distributed Computations and their Proofs Project

Previously, postdoc at Tsinghua University - LIAMA - Beijing.
INRIA - FORMES project

Previously, Ph.D. student under the supervision of Jean-Pierre Jouanaud.
TypiCal (ex. LogiCal) team - INRIA Saclay - Ile de France - Laboratoire d'Informatique de l'X

Office:
INRIA Futurs
Parc Club Orsay Université, Bât I - ZAC des Vignes
2-4, rue Jacques Monod
91893 ORSAY Cedex
France

Phone: +33 (0)1 69 35 69 90

EMail: pierre-yves [at] strub.nu

Research

Software

A Formalization of Elliptic Curves in Coq

Have a look at the dedicated page.

Publications

Coq Bundle

Coq Bundle is a Windows installer for the Coq proof assistant (8.3pl2) including mingw (gcc 4.5.2), ocaml (3.12.0), camlp5 (5.15), Ssreflect (1.3pl2), emacs (23.3), and ProofGeneral (4.1).

Download Coq Bundle.

Teaching