Introducing VAUCANSON. - Sylvain Lombardy; Raphael Poss; Yann Régis-Gianas; Jacques Sakarovitch (CIAA, 2003)

Introducing VAUCANSON. - Sylvain Lombardy; Yann Régis-Gianas; Jacques Sakarovitch (Theor. Comput. Sci., 2004)

Towards Efficient, Typed LR Parsers. - François Pottier; Yann Régis-Gianas (ML, 2005)

Stratified type inference for generalized algebraic data types. - François Pottier; Yann Régis-Gianas (POPL, 2006)

From types to logical assertions : automatic or assisted proofs of property about functional programs. (Des types aux assertions logiques : preuve automatique ou assistée de propriétés sur les programmes fonctionnels). - Yann Régis-Gianas (2007)

A Hoare Logic for Call-by-Value Functional Programs. - Yann Régis-Gianas; François Pottier (MPC, 2008)

Certifying cost annotations in compilers - Roberto M. Amadio; Nicholas Ayache; Yann Régis-Gianas; Ronan Saillard (CoRR, 2010)

Certifying and Reasoning on Cost Annotations of Functional Programs. - Roberto M. Amadio; Yann Régis-Gianas (FOPARA, 2011)

Certified Complexity. - R. Armadio; Andrea Asperti; Nicholas Ayache; Brian Campbell 001; Dominic P. Mulligan; Randy Pollack; Yann Régis-Gianas; Claudio Sacerdoti Coen; Ian Stark (FET, 2011)

Certifying and Reasoning on Cost Annotations in C Programs. - Nicholas Ayache; Roberto M. Amadio; Yann Régis-Gianas (FMICS, 2012)

Certified Complexity (CerCo). - Roberto M. Amadio; Nicholas Ayache; François Bobot; Jaap Boender; Brian Campbell 001; Ilias Garnier; Antoine Madet; James McKinna; Dominic P. Mulligan; Mauro Piccolo; Randy Pollack; Yann Régis-Gianas; et al. (FOPARA, 2013)

Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation. - Guillaume Claret; Lourdes Del Carmen González-Huesca; Yann Régis-Gianas; Beta Ziliani (ITP, 2013)

Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems. - Bruno Barras; Lourdes Del Carmen González-Huesca; Hugo Herbelin; Yann Régis-Gianas; Enrico Tassi; Makarius Wenzel; Burkhart Wolff (MKM/Calculemus/DML, 2013)

A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences. - Thibaut Girka; David Mentré; Yann Régis-Gianas (ATVA, 2015)

Mechanical Verification of Interactive Programs Specified by Use Cases. - Guillaume Claret; Yann Régis-Gianas (FormaliSE@ICSE, 2015)

Verifiable semantic difference languages. - Thibaut Girka; David Mentré; Yann Régis-Gianas (PPDP, 2017)

Copattern matching and first-class observations in OCaml, with a macro. - Paul Laforgue; Yann Régis-Gianas (PPDP, 2017)

Modular Verification of Programs with Effects and Effect Handlers in Coq. - Thomas Letan; Yann Régis-Gianas; Pierre Chifflier; Guillaume Hiet (FM, 2018)

Mtac2: typed tactics for backward reasoning in Coq. - Jan-Oliver Kaiser; Beta Ziliani; Robbert Krebbers; Yann Régis-Gianas; Derek Dreyer (Proc. ACM Program. Lang., 2018)

About some Metamorphoses of Computer Programs. (A propos de quelques métamorphoses des programmes informatiques). - Yann Régis-Gianas (2019)

Incremental lambda -Calculus in Cache-Transfer Style - Static Memoization by Program Transformation. - Paolo G. Giarrusso; Yann Régis-Gianas; Philipp Schuster (ESOP, 2019)

FreeSpec: specifying, verifying, and executing impure computations in Coq. - Thomas Letan; Yann Régis-Gianas (CPP, 2020)

Analysing installation scenarios of Debian packages. - Benedikt F. H. Becker; Nicolas Jeannerod; Claude Marché; Yann Régis-Gianas; Mihaela Sighireanu; Ralf Treinen (TACAS (2), 2020)

Morbig: A Static parser for POSIX shell. - Yann Régis-Gianas; Nicolas Jeannerod; Ralf Treinen (J. Comput. Lang., 2020)

Modular verification of programs with effects and effects handlers. - Thomas Letan; Yann Régis-Gianas; Pierre Chifflier; Guillaume Hiet (Formal Aspects Comput., 2021)

The CoLiS platform for the analysis of maintainer scripts in Debian software packages. - Benedikt F. H. Becker; Nicolas Jeannerod; Claude Marché; Yann Régis-Gianas; Mihaela Sighireanu; Ralf Treinen (Int. J. Softw. Tools Technol. Transf., 2022)