| A contraction theory approach to stochastic incremental stability QC Pham, N Tabareau, JJ Slotine IEEE Transactions on Automatic Control 54 (4), 816-820, 2009 | 173 | 2009 |
| How synchronization protects from noise N Tabareau, JJ Slotine, QC Pham PLoS computational biology 6 (1), e1000637, 2010 | 118 | 2010 |
| Coq coq correct! verification of type checking and erasure for coq, in coq M Sozeau, S Boulier, Y Forster, N Tabareau, T Winterhalter Proceedings of the ACM on Programming Languages 4 (POPL), 1-28, 2019 | 85 | 2019 |
| The metacoq project M Sozeau, A Anand, S Boulier, C Cohen, Y Forster, F Kunze, G Malecha, ... Journal of automated reasoning 64 (5), 947-999, 2020 | 80 | 2020 |
| The next 700 syntactical models of type theory S Boulier, PM Pédrot, N Tabareau Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and …, 2017 | 76 | 2017 |
| Resource modalities in tensor logic PA Melliès, N Tabareau Annals of Pure and Applied Logic 161 (5), 632-653, 2010 | 75 | 2010 |
| Where neuroscience and dynamic system theory meet autonomous robotics: a contracting basal ganglia model for action selection B Girard, N Tabareau, QC Pham, A Berthoz, JJ Slotine Neural Networks 21 (4), 628-641, 2008 | 73 | 2008 |
| Universe Polymorphism in Coq M Sozeau, N Tabareau Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as …, 2014 | 71 | 2014 |
| Definitional proof-irrelevance without K G Gilbert, J Cockx, M Sozeau, N Tabareau Proceedings of the ACM on Programming Languages 3 (POPL), 1-28, 2019 | 65 | 2019 |
| Towards Certified Meta-Programming with Typed Template-Coq A Anand, S Boulier, C Cohen, M Sozeau, N Tabareau Interactive Theorem Proving: 9th International Conference, ITP 2018, Held as …, 2018 | 59 | 2018 |
| An explicit formula for the free exponential modality of linear logic PA Melliès, N Tabareau, C Tasson Automata, Languages and Programming: 36th Internatilonal Collogquium, ICALP …, 2009 | 56 | 2009 |
| Extending type theory with forcing G Jaber, N Tabareau, M Sozeau 2012 27th Annual IEEE Symposium on Logic in Computer Science, 395-404, 2012 | 48 | 2012 |
| Geometry of the superior colliculus mapping and efficient oculomotor computation N Tabareau, D Bennequin, A Berthoz, JJ Slotine, B Girard Biological cybernetics 97, 279-292, 2007 | 47 | 2007 |
| Compiling functional types to relational specifications for low level imperative code N Benton, N Tabareau Proceedings of the 4th international workshop on Types in language design …, 2009 | 43 | 2009 |
| On timed automata with input-determined guards D d’Souza, N Tabareau Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant …, 2004 | 43 | 2004 |
| Equivalences for free: univalent parametricity for effective transport N Tabareau, É Tanter, M Sozeau Proceedings of the ACM on Programming Languages 2 (ICFP), 1-29, 2018 | 40 | 2018 |
| Failure is Not an Option: An Exceptional Type Theory PM Pédrot, N Tabareau Programming Languages and Systems: 27th European Symposium on Programming …, 2018 | 39 | 2018 |
| An effectful way to eliminate addiction to dependence PM Pédrot, N Tabareau 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-12, 2017 | 39 | 2017 |
| The definitional side of the forcing G Jaber, G Lewertowski, PM Pédrot, M Sozeau, N Tabareau Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer …, 2016 | 36 | 2016 |
| Gradual certified programming in Coq É Tanter, N Tabareau Proceedings of the 11th Symposium on Dynamic Languages, 26-40, 2015 | 33 | 2015 |
Matthieu SozeauResarcher, Inria Paris and PPSVerified email at inria.fr
