Aurèle Barrière

aurele.barriere@epfl.ch +41 21 693 88 46 https://aurele-barriere.github.io/

+41 21 693 88 46
Office:  INN 317
EPFL > IC > IINFCOM > SYSTEMF

Web site:  Web site:  https://systemf.epfl.ch/

+41 21 693 88 46
EPFL > VPA-AVP-PGE > AVP-PGE-EDOC > EDIC-ENS

vCard
Administrative data

Teaching & PhD

Courses

Interactive theorem proving

A hands-on introduction to interactive theorem proving, computer-checked mathematics, compiler verification, proofs as programs, dependent types, and proof automation. Come learn how to write computer-checked proofs and certified bug-free code!