Matthieu Sozeau
From MaRDI portal
List of research outcomes
This list is not complete and representing at the moment only items from zbMATH Open and arXiv. We are working on additional sources - please check back here soon!
| Publication | Date of Publication | Type |
|---|---|---|
| Correct and complete type checking and certified erasure for \textsc{Coq}, in \textsc{Coq} Journal of the ACM | 2026-02-24 | Paper |
| The Marriage of Univalence and Parametricity Journal of the ACM | 2022-12-08 | Paper |
| Cumulative inductive types in Coq | 2021-06-15 | Paper |
| Types are Internal $\infty$-Groupoids | 2021-04-30 | Paper |
| The \textsc{MetaCoq} project Journal of Automated Reasoning | 2020-11-02 | Paper |
| Towards certified meta-programming with typed Template-Coq | 2018-10-04 | Paper |
| The definitional side of the forcing Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science | 2018-04-23 | Paper |
| A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading Journal of Functional Programming | 2017-10-23 | Paper |
| Extending type theory with forcing 2012 27th Annual IEEE Symposium on Logic in Computer Science | 2017-05-16 | Paper |
| A unification algorithm for Coq featuring universe polymorphism and overloading Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming | 2017-05-10 | Paper |
| The HoTT Library: A formalization of homotopy type theory in Coq | 2016-10-14 | Paper |
| Partiality and recursion in interactive theorem provers -- an overview Mathematical Structures in Computer Science | 2016-07-28 | Paper |
| Universe polymorphism in Coq Interactive Theorem Proving | 2014-09-08 | Paper |
| Program-ing finger trees in Coq Proceedings of the 12th ACM SIGPLAN international conference on Functional programming | 2014-07-21 | Paper |
| A new look at generalized rewriting in type theory | 2011-02-10 | Paper |
| Equations: a dependent pattern-matching compiler Interactive Theorem Proving | 2010-09-14 | Paper |
| Subset Coercions in Coq Lecture Notes in Computer Science | 2009-03-10 | Paper |
| First-Class Type Classes Lecture Notes in Computer Science | 2008-12-04 | Paper |
Research outcomes over time
This page was built for person: Matthieu Sozeau
