| 2020 | CPP | FreeSpec: specifying, verifying, and executing impure computations in Coq. | Thomas Letan, Yann Rgis-Gianas |
| 2020 | TACAS | Analysing installation scenarios of Debian packages. | Benedikt F. H. Becker, Nicolas Jeannerod, Claude March, Yann Rgis-Gianas, Mihaela Sighireanu, Ralf Treinen |
| 2019 | ESOP | Incremental \lambda -Calculus in Cache-Transfer Style - Static Memoization by Program Transformation. | Paolo G. Giarrusso, Yann Rgis-Gianas, Philipp Schuster |
| 2018 | FM | Modular Verification of Programs with Effects and Effect Handlers in Coq. | Thomas Letan, Yann Rgis-Gianas, Pierre Chifflier, Guillaume Hiet |
| 2018 | SLE | Morbig: a static parser for POSIX shell. | Yann Rgis-Gianas, Nicolas Jeannerod, Ralf Treinen |
| 2017 | PPDP | Verifiable semantic difference languages. | Thibaut Girka, David Mentr, Yann Rgis-Gianas |
| 2017 | PPDP | Copattern matching and first-class observations in OCaml, with a macro. | Paul Laforgue, Yann Rgis-Gianas |
| 2015 | ATVA | A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences. | Thibaut Girka, David Mentr, Yann Rgis-Gianas |
| 2015 | ICSE | Mechanical Verification of Interactive Programs Specified by Use Cases. | Guillaume Claret, Yann Rgis-Gianas |
| 2013 | ITP | Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation. | Guillaume Claret, Lourdes Del Carmen Gonzlez-Huesca, Yann Rgis-Gianas, Beta Ziliani |
| 2012 | FMICS | Certifying and Reasoning on Cost Annotations in C Programs. | Nicholas Ayache, Roberto M. Amadio, Yann Rgis-Gianas |
| 2008 | MPC | A Hoare Logic for Call-by-Value Functional Programs. | Yann Rgis-Gianas, Franois Pottier |
| 2006 | POPL | Stratified type inference for generalized algebraic data types. | Franois Pottier, Yann Rgis-Gianas |