2022
Journal articles
- titre
- The CoLiS Platform for the Analysis of Maintainer Scripts in Debian Software Packages
- auteur
- Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, Ralf Treinen
- article
- International Journal on Software Tools for Technology Transfer, 2022
- Accès au texte intégral et bibtex
-
2021
Books
- titre
- JFLA 2021 - 32 èmes Journées Francophones des Langages Applicatifs
- auteur
- Yann Regis-Gianas, Chantal Keller
- article
- 2021
- Accès au texte intégral et bibtex
-
2020
Journal articles
- titre
- Modular verification of programs with effects and effects handlers
- auteur
- Thomas Letan, Yann Régis-Gianas, Pierre Chifflier, Guillaume Hiet
- article
- Formal Aspects of Computing, 2020, ⟨10.1007/s00165-020-00523-2⟩
- Accès au bibtex
-
Conference papers
- titre
- Analysing installation scenarios of Debian packages
- auteur
- Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, Ralf Treinen
- article
- TACAS 2020 - 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr 2020, The conference took place on-line, because it couldn't be held in Dublin, Ireland. pp.235-253, ⟨10.1007/978-3-030-45237-7_14⟩
- Accès au texte intégral et bibtex
-
- titre
- FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq
- auteur
- Thomas Letan, Yann Régis-Gianas
- article
- CPP 2020 - 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2020, Nouvelle-Orléans, United States. pp.1-15, ⟨10.1145/3372885.3373812⟩
- Accès au texte intégral et bibtex
-
Books
- titre
- 31ème Journées Francophones des Langages Applicatifs
- auteur
- Zaynah Lea Dargaye, Yann Regis-Gianas
- article
- IRIF, 2020
- Accès au texte intégral et bibtex
-
2019
Conference papers
- titre
- Learn-OCaml : un assistant à l'enseignement d'OCaml
- auteur
- Cagdas Bozman, Benjamin Canou, Roberto Di Cosmo, Pierrick Couderc, Louis Gesbert, Grégoire Henry, Fabrice Le Fessant, Michel Mauny, Carine Morel, Loïc Peyrot, Yann Regis-Gianas
- article
- JFLA 2019 - Journées Francophones des Langages Applicatifs, Jan 2019, Les Rousses, France
- Accès au texte intégral et bibtex
-
- titre
- Incremental λ-Calculus in Cache-Transfer Style Static Memoization by Program Transformation
- auteur
- Paolo G Giarrusso, Yann Régis-Gianas, Philipp Schuster
- article
- ESOP 2019 - European Symposium on Programming, Apr 2019, Prague, Czech Republic
- Accès au texte intégral et bibtex
-
Habilitation à diriger des recherches
- titre
- About some Metamorphoses of Computer Programs
- auteur
- Yann Regis-Gianas
- article
- Programming Languages [cs.PL]. Université Paris Diderot, 2019
- Accès au texte intégral et bibtex
-
Reports
- titre
- Specification of UNIX Utilities
- auteur
- Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, Ralf Treinen
- article
- [Technical Report] ANR. 2019
- Accès au texte intégral et bibtex
-
2018
Journal articles
- titre
- Mtac2: typed tactics for backward reasoning in Coq
- auteur
- Jan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann Régis-Gianas, Derek Dreyer
- article
- Proceedings of the ACM on Programming Languages, 2018, 2 (ICFP), pp.1 - 31. ⟨10.1145/3236773⟩
- Accès au bibtex
-
Conference papers
- titre
- Morbig: A Static Parser for POSIX Shell
- auteur
- Yann Régis-Gianas, Nicolas Jeannerod, Ralf Treinen
- article
- SLE 2018 - ACM SIGPLAN International Conference on Software Language Engineering, Nov 2018, Boston, United States. ⟨10.1145/3276604.3276615⟩
- Accès au texte intégral et bibtex
-
- titre
- OCaml étendu avec du filtrage par comotifs
- auteur
- Paul Laforgue, Yann Régis-Gianas
- article
- JFLA 2018 - Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls sur mer, France
- Accès au texte intégral et bibtex
-
- titre
- Modular Verification of Programs with Effects and Effect Handlers in Coq
- auteur
- Thomas Letan, Yann Régis-Gianas, Pierre Chifflier, Guillaume Hiet
- article
- FM 2018 - 22nd International Symposium on Formal Methods, Jul 2018, Oxford, United Kingdom. pp.338-354, ⟨10.1007/978-3-319-95582-7_20⟩
- Accès au texte intégral et bibtex
-
Software
- titre
- Correlating Oracles
- auteur
- Thibaut Girka, Yann Régis-Gianas
- article
- 2018, ⟨swh:1:dir:2c01e745c6d89e0eeb9a6ec9590f7ef0750b7002;origin=https://hal.archives-ouvertes.fr/hal-01831369;visit=swh:1:snp:42f0897956e700a23f5b8aafce43360b8699c0f1;anchor=swh:1:rev:698771f9ca7ce7605fdcabf27b5851f322ea692c;path=/⟩
- Accès au texte intégral et bibtex
-
- titre
- Morbig
- auteur
- Yann Regis-Gianas, Nicolas Jeannerod, Ralf Treinen
- article
- 2018, ⟨swh:1:dir:eb7770ebd7341d08d8dc17f5257ed17852a015a8;origin=https://hal.archives-ouvertes.fr/hal-01897572;visit=swh:1:snp:e3b0b9991945262e7cc28768373af4560caf7afa;anchor=swh:1:rev:ad0c16675d221938530269610308cd5a2c142687;path=/⟩
- Accès au texte intégral et bibtex
-
2017
Conference papers
- titre
- Verifiable Semantic Difference Languages
- auteur
- Thibaut Girka, David Mentré, Yann Régis-Gianas
- article
- International Symposium on Principles and Practice of Declarative Programming, Oct 2017, Namur, Belgium. ⟨10.1145/3131851.3131870⟩
- Accès au texte intégral et bibtex
-
- titre
- Copattern matching and first-class observations in OCaml, with a macro
- auteur
- Paul Laforgue, Yann Régis-Gianas
- article
- International Symposium on Principles and Practice of Declarative Programming, Oct 2017, Namur, Belgium. ⟨10.1145/3131851.3131869⟩
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- titre
- Having Fun With 31.521 Shell Scripts
- auteur
- Nicolas Jeannerod, Yann Régis-Gianas, Ralf Treinen
- article
- 2017
- Accès au texte intégral et bibtex
-
2016
Reports
- titre
- Oracle-based Differential Operational Semantics (long version)
- auteur
- Thibaut Girka, David Mentré, Yann Régis-Gianas
- article
- [Research Report] Université Paris Diderot / Sorbonne Paris Cité. 2016
- Accès au texte intégral et bibtex
-
2015
Conference papers
- titre
- A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences
- auteur
- Thibaut Girka, David Mentré, Yann Régis-Gianas
- article
- Automated Technology for Verification and Analysis, Oct 2015, Shanghai, China. ⟨10.1007/978-3-319-24953-7_6⟩
- Accès au texte intégral et bibtex
-
- titre
- Mechanical Verification of Interactive Programs Specified by Use Cases
- auteur
- Guillaume Claret, Yann Régis-Gianas
- article
- 3rd IEEE/ACM FME Workshop on Formal Methods in Software Engineering, May 2015, Florence, Italy. ⟨10.1109/FormaliSE.2015.17⟩
- Accès au texte intégral et bibtex
-
2014
Reports
- titre
- Coq 8.4 Reference Manual
- auteur
- Pierre Boutillier, Stephane Glondu, Benjamin Grégoire, Hugo Herbelin, Pierre Letouzey, Pierre-Marie Pédrot, Yann Régis-Gianas, Matthieu Sozeau, Arnaud Spiwack, Enrico Tassi
- article
- [Research Report] Inria. 2014
- Accès au bibtex
-
2013
Journal articles
- titre
- Certifying and reasoning about cost annotations of functional programs
- auteur
- Roberto M. Amadio, Yann Régis-Gianas
- article
- Higher-Order and Symbolic Computation, 2013
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems
- auteur
- Bruno Barras, Lourdes del Carmen Gonzalez Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff
- article
- MKM/Calculemus/DML, Jul 2013, Bath, United Kingdom. pp.359-363
- Accès au bibtex
-
- titre
- Lightweight proof by reflection using a posteriori simulation of effectful computation
- auteur
- Guillaume Claret, Lourdes del Carmen Gonzalez Huesca, Yann Régis-Gianas, Beta Ziliani
- article
- Interactive Theorem Proving, Jul 2013, Rennes, France
- Accès au texte intégral et bibtex
-
2012
Conference papers
- titre
- Safe Incremental Type Checking
- auteur
- Matthias Puech, Yann Régis-Gianas
- article
- TLDI 2012 - Seventh ACM SIGPLAN Workshop on Types in Language Design and Implementation, Jan 2012, Philadelphia, United States
- Accès au texte intégral et bibtex
-
- titre
- Certifying and reasoning on cost annotations in C programs
- auteur
- Nicolas Ayache, Roberto Amadio, Yann Régis-Gianas
- article
- FMICS 2012 - 17th International Workshop on Formal Methods for Industrial Critical Systems, Aug 2012, Paris, France
- Accès au texte intégral et bibtex
-
2010
Conference papers
- titre
- Towards typed repositories of proofs
- auteur
- Matthias Puech, Yann Régis-Gianas
- article
- Mathematically Intelligent Proof Search - MIPS 2010, Jul 2010, Paris, France
- Accès au texte intégral et bibtex
-
Reports
- titre
- Certifying cost annotations in compilers
- auteur
- Roberto M. Amadio, Nicolas Ayache, Yann Régis-Gianas, Ronan Saillard
- article
- 2010
- Accès au texte intégral et bibtex
-
2008
Conference papers
- titre
- A Hoare Logic for Call-by-Value Functional Programs
- auteur
- Yann Régis-Gianas, François Pottier
- article
- MPC 08 - Proceedings of the Ninth International Conference on Mathematics of Program Construction, Jul 2008, Marseille, France. pp.305--335, ⟨10.1007/978-3-540-70594-9_17⟩
- Accès au bibtex
-
2007
Theses
- titre
- From types to logical assertions : automatic or assisted proofs of property about functional programs
- auteur
- Yann Régis-Gianas
- article
- Programming Languages [cs.PL]. Université paris diderot, 2007. English. ⟨NNT : 2007PA077155⟩
- Accès au texte intégral et bibtex
-
2006
Conference papers
- titre
- Stratified type inference for generalized algebraic data types
- auteur
- François Pottier, Yann Régis-Gianas
- article
- POPL'06 - Proceedings of the 33rd ACM Symposium on Principles of Programming Languages, Jan 2006, Charleston, South Carolina, United States. pp.232--244
- Accès au bibtex
-
- titre
- Towards efficient, typed LR parsers.
- auteur
- François Pottier, Yann Régis-Gianas
- article
- ACM Workshop on ML, Mar 2006, Portland, Oregon, United States
- Accès au bibtex
-
2004
Journal articles
- titre
- Introducing Vaucanson
- auteur
- Sylvain Lombardy, Yann Regis-Gianas, Jacques Sakarovitch
- article
- Theoretical Computer Science, 2004, 328, pp.77-96. ⟨10.1016/j.tcs.2004.07.007⟩
- Accès au bibtex
-
2003
Conference papers
- titre
- Introducing Vaucanson
- auteur
- Sylvain Lombardy, Raphaël Poss, Yann Régis-Gianas, Jacques Sakarovitch
- article
- 8th International Conference on Implementation and Application of Automata (CIAA 2003), Jul 2003, Santa Barbara, California, USA, United States. pp.96-107
- Accès au bibtex
-