Publications HAL de Regis-Gianas

2021

Directions of work or proceedings

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
https://hal.archives-ouvertes.fr/hal-03190426/file/proceedings-jfla-2021.pdf 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, Springer Verlag, 2020, ⟨10.1007/s00165-020-00523-2⟩
Accès au bibtex
BibTex

Conference papers

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
https://hal.inria.fr/hal-02422273/file/article.pdf BibTex
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
https://hal.archives-ouvertes.fr/hal-02355602/file/main.pdf BibTex

Directions of work or proceedings

titre
31ème Journées Francophones des Langages Applicatifs
auteur
Zaynah Dargaye, Yann Regis-Gianas
article
IRIF, 2020
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02427360/file/proceedings-jfla-2020.pdf BibTex

2019

Conference papers

titre
Incremental λ-Calculus in Cache-Transfer Style Static Memoization by Program Transformation
auteur
Paolo 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
https://hal.inria.fr/hal-02405864/file/giarusso19incremental.pdf BibTex
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
https://hal.inria.fr/hal-01962838/file/main.pdf 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
https://hal.inria.fr/tel-02405839/file/hdr.pdf 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
https://hal.inria.fr/hal-02321691/file/main.pdf 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, ACM, 2018, 2 (ICFP), pp.1 - 31. ⟨10.1145/3236773⟩
Accès au bibtex
BibTex

Conference papers

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
https://hal.inria.fr/hal-01897456/file/paper.pdf BibTex
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
https://hal.archives-ouvertes.fr/hal-01890044/file/main.pdf 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
https://hal.inria.fr/hal-01799712/file/main.pdf BibTex

Software

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
https://hal.inria.fr/hal-01897572/file/morbig-0.9.1.zip BibTex
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
https://hal.inria.fr/hal-01831369/file/CorrelatingProgram.zip BibTex

2017

Conference papers

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
https://hal.inria.fr/hal-01653261/file/laforgue-17.pdf BibTex
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
https://hal.inria.fr/hal-01653283/file/girka-16.pdf 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
https://hal.archives-ouvertes.fr/hal-01513750/file/main.pdf 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
https://hal.inria.fr/hal-01419860/file/long-version.pdf BibTex

2015

Conference papers

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
https://hal.inria.fr/hal-01255107/file/index.pdf BibTex
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
https://hal.inria.fr/hal-01238704/file/root.pdf 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
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, Springer Verlag, 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00629473/file/main.pdf 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
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
https://hal.inria.fr/hal-00870110/file/simulation-based-pbr-final.pdf BibTex

2012

Conference papers

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
https://hal.inria.fr/hal-00702665/file/ccac-fmics-final.pdf BibTex
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
https://hal.archives-ouvertes.fr/hal-00650341/file/abstract.pdf 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
https://hal.inria.fr/inria-00525874/file/puech-regis-gianas-mips-2010.pdf 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
https://hal.archives-ouvertes.fr/hal-00524715/file/ccac-hal.pdf 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
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
https://hal.inria.fr/tel-01238703/file/these-yann.regis-gianas.pdf BibTex

2006

Conference papers

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
BibTex
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
BibTex

2004

Journal articles

titre
Introducing Vaucanson
auteur
Sylvain Lombardy, Yann Regis-Gianas, Jacques Sakarovitch
article
Theoretical Computer Science, Elsevier, 2004, 328, pp.77-96. ⟨10.1016/j.tcs.2004.07.007⟩
Accès au bibtex
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
BibTex