( en | de | ru )

 

Disambiguation of "Sozeau, Matthieu"

Author of the publication

copydeleteadd this publication to your clipboard
The Multiverse: Logical Modularity for Proof Assistants.

, , , , and . CoRR, (2021)

Please choose a person to relate this publication to

To differ between persons with the same name, the academic degree and the title of an important publication will be displayed. You can also use the button next to the name to display some publications already assigned to the person.

Matthieu Saubanère

Matthieu Hammer

Matthieu Felsinger

Friedrich Matthieu

Matthieu Barukinamwo

 

Other publications of authors with the same name

Coq Coq correct! verification of type checking and erasure for Coq, in Coq., , , , and . Proc. ACM Program. Lang., 4 (POPL): 8:1-8:28 (2020)Subset Coercions in Coq. TYPES'06, volume 4502 of Lecture Notes in Computer Science, page 237-252. Springer, (2007)Equations for Hereditary Substitution in Leivant's Predicative System F: A Case Study., and . CoRR, (2015)First-Class Type Classes., and . TPHOLs, volume 5170 of Lecture Notes in Computer Science, page 278-293. Springer, (2008)Universe Polymorphism in Coq., and . ITP, volume 8558 of Lecture Notes in Computer Science, page 499-514. Springer, (2014)Equations reloaded: high-level dependently-typed functional programming and proving in Coq., and . Proc. ACM Program. Lang., 3 (ICFP): 86:1-86:29 (2019)Un environnement pour la programmation avec types dépendants. Université Paris 11, Orsay, France, (December 2008)Definitional proof-irrelevance without K., , , and . Proc. ACM Program. Lang., 3 (POPL): 3:1-3:28 (2019)The MetaCoq Project., , , , , , , , and . J. Autom. Reason., 64 (5): 947-999 (2020)Touring the MetaCoq Project (Invited Paper).. LFMTP, volume 337 of EPTCS, page 13-29. (2021)