Vincent Laporte

Research Engineer at Inria, working on the Coq proof assistant.

E-mail: Vincent [dot] Laporte [at] mailbox [dot] org

PGP: EBD582AD DDB1F81F

Phone: 0 (033) 2 99 84 74 54

Work address:

Campus universitaire de Beaulieu
35042 Rennes Cedex

Curriculum vitæ (pdf, 67 Kio).

Publications

See dblp for a complete list.

Selected publications

Research projects

Jasmin

Jasmin is a programming language to write high-assurance, high-speed cryptographic implementations.

Its compiler is correct — formally verified in Coq.

Verasco

Verasco is a formally-verified static analyzer for C.