Yann Régis-Gianas

29 papers A* 1A 1B 6C 4Journal 8Unranked 7

Year	Rank	Type	Title / Venue / Authors
2022	J	`jnl`	The CoLiS platform for the analysis of maintainer scripts in Debian software packages. Int. J. Softw. Tools Technol. Transf. Benedikt F. H. Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, Ralf Treinen
2021	J	`jnl`	Modular verification of programs with effects and effects handlers. Formal Aspects Comput. Thomas Letan, Yann Régis-Gianas, Pierre Chifflier, Guillaume Hiet
2020	—	`conf`	Analysing installation scenarios of Debian packages. TACAS (2) Benedikt F. H. Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, Ralf Treinen
2020	B	`conf`	FreeSpec: specifying, verifying, and executing impure computations in Coq. CPP Thomas Letan, Yann Régis-Gianas
2020	J	`jnl`	Morbig: A Static parser for POSIX shell. J. Comput. Lang. Yann Régis-Gianas, Nicolas Jeannerod, Ralf Treinen
2019	—	`book`	About some Metamorphoses of Computer Programs. (A propos de quelques métamorphoses des programmes informatiques). Yann Régis-Gianas
2019	A	`conf`	Incremental \lambda -Calculus in Cache-Transfer Style - Static Memoization by Program Transformation. ESOP Paolo G. Giarrusso, Yann Régis-Gianas, Philipp Schuster
2018	B	`conf`	Modular Verification of Programs with Effects and Effect Handlers in Coq. FM Thomas Letan, Yann Régis-Gianas, Pierre Chifflier, Guillaume Hiet
2018	B	`conf`	Morbig: a static parser for POSIX shell. SLE Yann Régis-Gianas, Nicolas Jeannerod, Ralf Treinen
2018	J	`jnl`	Mtac2: typed tactics for backward reasoning in Coq. Proc. ACM Program. Lang. Jan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann Régis-Gianas, Derek Dreyer
2017	C	`conf`	Copattern matching and first-class observations in OCaml, with a macro. PPDP Paul Laforgue, Yann Régis-Gianas
2017	C	`conf`	Verifiable semantic difference languages. PPDP Thibaut Girka, David Mentré, Yann Régis-Gianas
2015	B	`conf`	A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences. ATVA Thibaut Girka, David Mentré, Yann Régis-Gianas
2015	—	`conf`	Mechanical Verification of Interactive Programs Specified by Use Cases. FormaliSE@ICSE Guillaume Claret, Yann Régis-Gianas
2013	—	`conf`	Certified Complexity (CerCo). FOPARA 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
2013	B	`conf`	Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation. ITP Guillaume Claret, Lourdes Del Carmen González-Huesca, Yann Régis-Gianas, Beta Ziliani
2013	—	`conf`	Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems. MKM/Calculemus/DML Bruno Barras, Lourdes Del Carmen González-Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff
2013	J	`jnl`	Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems. CoRR Bruno Barras, Lourdes Del Carmen González-Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff
2012	C	`conf`	Certifying and Reasoning on Cost Annotations in C Programs. FMICS Nicholas Ayache, Roberto M. Amadio, Yann Régis-Gianas
2011	—	`conf`	Certified Complexity. FET R. Armadio, Andrea Asperti, Nicholas Ayache, Brian Campbell, Dominic P. Mulligan, Randy Pollack, Yann Régis-Gianas, Claudio Sacerdoti Coen, Ian Stark
2011	—	`conf`	Certifying and Reasoning on Cost Annotations of Functional Programs. FOPARA Roberto M. Amadio, Yann Régis-Gianas
2011	J	`jnl`	Certifying and reasoning on cost annotations of functional programs CoRR Roberto M. Amadio, Yann Régis-Gianas
2010	J	`jnl`	Certifying cost annotations in compilers CoRR Roberto M. Amadio, Nicholas Ayache, Yann Régis-Gianas, Ronan Saillard
2008	B	`conf`	A Hoare Logic for Call-by-Value Functional Programs. MPC Yann Régis-Gianas, François Pottier
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
2006	A*	`conf`	Stratified type inference for generalized algebraic data types. POPL François Pottier, Yann Régis-Gianas
2005	—	`conf`	Towards Efficient, Typed LR Parsers. ML François Pottier, Yann Régis-Gianas
2004	J	`jnl`	Introducing VA Theor. Comput. Sci. Sylvain Lombardy, Yann Régis-Gianas, Jacques Sakarovitch
2003	C	`conf`	Introducing VAUCANSON. CIAA Sylvain Lombardy, Raphael Poss, Yann Régis-Gianas, Jacques Sakarovitch