Past Member
Matthieu Sozeau
Funding provided by the Charles Simonyi Endowment
Affiliation
Mathematics
Field of Study
Computer Science
From
–
Matthieu Sozeau is one of the main developers of the Coq proof-assistant, currently used as the basis of the univalent foundations program. His plan is to work on adapting the theory and implementation of Coq to homotopy type theory, including an adequate universe system and facilities for rewriting and proving in this new setting.
Dates at IAS
Member
School of Mathematics
–
Fall
Degrees
University of Paris XI, Paris Sud
Ph.D.
2008