Yann Régis-Gianas

According to our database, Yann Régis-Gianas authored at least 26 papers between 2003 and 2022.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2022

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

2021

Modular verification of programs with effects and effects handlers.

Thomas Letan, Yann Régis-Gianas, Pierre Chifflier, Guillaume Hiet

Formal Aspects Comput., 2021

2020

Morbig: A Static parser for POSIX shell.

Yann Régis-Gianas, Nicolas Jeannerod, Ralf Treinen

J. Comput. Lang., 2020

Analysing installation scenarios of Debian packages.

Benedikt F. H. Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, Ralf Treinen

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

FreeSpec: specifying, verifying, and executing impure computations in Coq.

Thomas Letan, Yann Régis-Gianas

Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

2019

Incremental \lambda -Calculus in Cache-Transfer Style - Static Memoization by Program Transformation.

Paolo G. Giarrusso, Yann Régis-Gianas, Philipp Schuster

Proceedings of the Programming Languages and Systems, 2019

About some Metamorphoses of Computer Programs. (A propos de quelques métamorphoses des programmes informatiques).

Yann Régis-Gianas

, 2019

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

Modular Verification of Programs with Effects and Effect Handlers in Coq.

Thomas Letan, Yann Régis-Gianas, Pierre Chifflier, Guillaume Hiet

Proceedings of the Formal Methods - 22nd International Symposium, 2018

2017

Copattern matching and first-class observations in OCaml, with a macro.

Paul Laforgue, Yann Régis-Gianas

Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, Namur, Belgium, October 09, 2017

Verifiable semantic difference languages.

Thibaut Girka, David Mentré, Yann Régis-Gianas

Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, Namur, Belgium, October 09, 2017

2015

Mechanical Verification of Interactive Programs Specified by Use Cases.

Guillaume Claret, Yann Régis-Gianas

Proceedings of the 3rd IEEE/ACM FME Workshop on Formal Methods in Software Engineering, 2015

A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences.

Thibaut Girka, David Mentré, Yann Régis-Gianas

Proceedings of the Automated Technology for Verification and Analysis, 2015

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

Proceedings of the Intelligent Computer Mathematics, 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

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

Certified Complexity (CerCo).

Roberto M. Amadio, Nicholas Ayache, François Bobot, Jaap Boender, Brian Campbell, Ilias Garnier, Antoine Madet, James McKinna, Dominic P. Mulligan, Mauro Piccolo, Randy Pollack, Yann Régis-Gianas, Claudio Sacerdoti Coen, Ian Stark, Paolo Tranquilli

Proceedings of the Foundational and Practical Aspects of Resource Analysis, 2013

2012

Certifying and Reasoning on Cost Annotations in C Programs.

Nicholas Ayache, Roberto M. Amadio, Yann Régis-Gianas

Proceedings of the Formal Methods for Industrial Critical Systems, 2012

2011

Certified Complexity.

R. Armadio, Andrea Asperti, Nicholas Ayache, Brian Campbell, Dominic P. Mulligan, Randy Pollack, Yann Régis-Gianas, Claudio Sacerdoti Coen, Ian Stark

Proceedings of the 2nd European Future Technologies Conference and Exhibition, 2011

Certifying and Reasoning on Cost Annotations of Functional Programs.

Roberto M. Amadio, Yann Régis-Gianas

Proceedings of the Foundational and Practical Aspects of Resource Analysis, 2011

2010

Certifying cost annotations in compilers

Roberto M. Amadio, Nicholas Ayache, Yann Régis-Gianas, Ronan Saillard

CoRR, 2010

2008

A Hoare Logic for Call-by-Value Functional Programs.

Yann Régis-Gianas, François Pottier

Proceedings of the Mathematics of Program Construction, 9th International Conference, 2008

2007

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

PhD thesis, 2007

2006

Stratified type inference for generalized algebraic data types.

François Pottier, Yann Régis-Gianas

Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2006

2005

Towards Efficient, Typed LR Parsers.

François Pottier, Yann Régis-Gianas

Proceedings of the ACM-SIGPLAN Workshop on ML, 2005

2004

Introducing VA_UCANSON.

Sylvain Lombardy, Yann Régis-Gianas, Jacques Sakarovitch

Theor. Comput. Sci., 2004

2003

Introducing VAUCANSON.

Sylvain Lombardy, Raphael Poss, Yann Régis-Gianas, Jacques Sakarovitch

Proceedings of the Implementation and Application of Automata, 2003