| Stratified type inference for generalized algebraic data types F Pottier, Y Régis-Gianas ACM SIGPLAN Notices 41 (1), 232-244, 2006 | 83 | 2006 |
| A Hoare logic for call-by-value functional programs Y Régis-Gianas, F Pottier International Conference on Mathematics of Program Construction, 305-335, 2008 | 71 | 2008 |
| Certified complexity (cerco) RM Amadio, N Ayache, F Bobot, JP Boender, B Campbell, I Garnier, ... Foundational and Practical Aspects of Resource Analysis: Third International …, 2014 | 50 | 2014 |
| Modular verification of programs with effects and effect handlers in Coq T Letan, Y Régis-Gianas, P Chifflier, G Hiet Formal Methods: 22nd International Symposium, FM 2018, Held as Part of the …, 2018 | 45* | 2018 |
| Introducing vaucanson S Lombardy, Y Régis-Gianas, J Sakarovitch Theoretical Computer Science 328 (1-2), 77-96, 2004 | 44 | 2004 |
| Mtac2: typed tactics for backward reasoning in Coq JO Kaiser, B Ziliani, R Krebbers, Y Régis-Gianas, D Dreyer Proceedings of the ACM on Programming Languages 2 (ICFP), 1-31, 2018 | 37 | 2018 |
| Lightweight proof by reflection using a posteriori simulation of effectful computation G Claret, L del Carmen González Huesca, Y Régis-Gianas, B Ziliani Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes …, 2013 | 29 | 2013 |
| Introducing Vaucanson S Lombardy, R Poss, Y Régis-Gianas, J Sakarovitch International Conference on Implementation and Application of Automata, 96-107, 2003 | 28 | 2003 |
| Towards efficient, typed LR parsers F Pottier, Y Régis-Gianas Electronic Notes in Theoretical Computer Science 148 (2), 155-180, 2006 | 25 | 2006 |
| FreeSpec: specifying, verifying, and executing impure computations in Coq T Letan, Y Régis-Gianas Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020 | 23 | 2020 |
| Pervasive parallelism in highly-trustable interactive theorem proving systems B Barras, L del Carmen González Huesca, H Herbelin, Y Régis-Gianas, ... Intelligent Computer Mathematics: MKM, Calculemus, DML, and Systems and …, 2013 | 21 | 2013 |
| Menhir reference manual F Pottier, Y Régis-Gianas Inria, Aug, 2016 | 20 | 2016 |
| On orthogonal specialization in C++: Dealing with efficiency and algebraic abstraction in Vaucanson Y Regis-Gianas, R Poss Proc. of POOSC 2003, 2003 | 19 | 2003 |
| Morbig: A static parser for POSIX shell Y Régis-Gianas, N Jeannerod, R Treinen Proceedings of the 11th ACM SIGPLAN International Conference on Software …, 2018 | 17 | 2018 |
| The Menhir parser generator F Pottier, Y Régis-Gianas See: http://gallium. inria. fr/fpottier/menhir, 2016 | 17 | 2016 |
| Incremental-Calculus in Cache-Transfer Style: Static Memoization by Program Transformation PG Giarrusso, Y Régis-Gianas, P Schuster European Symposium on Programming, 553-580, 2019 | 14 | 2019 |
| Certifying and reasoning on cost annotations in C programs N Ayache, RM Amadio, Y Régis-Gianas Formal Methods for Industrial Critical Systems: 17th International Workshop …, 2012 | 14 | 2012 |
| Certifying and reasoning on cost annotations of functional programs RM Amadio, Y Régis-Gianas International Workshop on Foundational and Practical Aspects of Resource …, 2011 | 14 | 2011 |
| Menhir F Pottier, Y Régis-Gianas URL http://gallium. inria. fr/~ fpottier/menhir, 2022 | 10 | 2022 |
| Certified complexity R Armadio, A Asperti, N Ayache, B Campbell, D Mulligan, R Pollack, ... Procedia Computer Science 7, 175-177, 2011 | 10 | 2011 |
Beta ZilianiFAMAF, UNC and Manas.TechVerified email at mpi-sws.org
