Skip to Main content Skip to Navigation


...
inria-00629473v2  Journal articles
Roberto M. AmadioYann Régis-Gianas. Certifying and reasoning about cost annotations of functional programs
Higher-Order and Symbolic Computation, Springer Verlag, 2013
...
hal-00702665v2  Conference papers
Nicolas AyacheRoberto M. AmadioYann Régis-Gianas. Certifying and reasoning on cost annotations in C programs
FMICS 2012 - 17th International Workshop on Formal Methods for Industrial Critical Systems, Aug 2012, Paris, France
...
hal-02355602v2  Conference papers
Benedikt BeckerNicolas JeannerodClaude MarchéYann Régis-GianasMihaela Sighireanu et al.  Analysing installation scenarios of Debian packages
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⟩
...
hal-01255107v1  Conference papers
Guillaume ClaretYann Régis-Gianas. Mechanical Verification of Interactive Programs Specified by Use Cases
3rd IEEE/ACM FME Workshop on Formal Methods in Software Engineering, May 2015, Florence, Italy. ⟨10.1109/FormaliSE.2015.17⟩
...
hal-02405864v1  Conference papers
Paolo GiarrussoYann Régis-GianasPhilipp Schuster. Incremental λ-Calculus in Cache-Transfer Style Static Memoization by Program Transformation
ESOP 2019 - European Symposium on Programming, Apr 2019, Prague, Czech Republic
...
hal-01653283v1  Conference papers
Thibaut GirkaDavid MentréYann Régis-Gianas. Verifiable Semantic Difference Languages
International Symposium on Principles and Practice of Declarative Programming, Oct 2017, Namur, Belgium. ⟨10.1145/3131851.3131870⟩
...
hal-01419860v1  Reports
Thibaut GirkaDavid MentréYann Régis-Gianas. Oracle-based Differential Operational Semantics (long version)
[Research Report] Université Paris Diderot / Sorbonne Paris Cité. 2016
hal-01890511v1  Journal articles
Jan-Oliver KaiserBeta ZilianiRobbert KrebbersYann Régis-GianasDerek Dreyer. Mtac2: typed tactics for backward reasoning in Coq
Proceedings of the ACM on Programming Languages, ACM, 2018, 2 (ICFP), pp.1 - 31. ⟨10.1145/3236773⟩
...
hal-01653261v1  Conference papers
Paul LaforgueYann Régis-Gianas. Copattern matching and first-class observations in OCaml, with a macro
International Symposium on Principles and Practice of Declarative Programming, Oct 2017, Namur, Belgium. ⟨10.1145/3131851.3131869⟩
...
hal-01897456v1  Conference papers
Paul LaforgueYann Régis-Gianas. OCaml étendu avec du filtrage par comotifs
JFLA 2018 - Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls sur mer, France
...
hal-02422273v1  Conference papers
Thomas LetanYann Régis-Gianas. FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq
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⟩
...
hal-01799712v1  Conference papers
Thomas LetanYann Régis-GianasPierre ChifflierGuillaume Hiet. Modular Verification of Programs with Effects and Effect Handlers in Coq
FM 2018 - 22nd International Symposium on Formal Methods, Jul 2018, Oxford, United Kingdom. pp.338-354, ⟨10.1007/978-3-319-95582-7_20⟩
inria-00629090v1  Conference papers
François PottierYann Régis-Gianas. Towards efficient, typed LR parsers.
ACM Workshop on ML, Mar 2006, Portland, Oregon, United States
inria-00629091v1  Conference papers
François PottierYann Régis-Gianas. Stratified type inference for generalized algebraic data types
POPL'06 - Proceedings of the 33rd ACM Symposium on Principles of Programming Languages, Jan 2006, Charleston, South Carolina, United States. pp.232--244
...
hal-00650341v1  Conference papers
Matthias PuechYann Régis-Gianas. Safe Incremental Type Checking
TLDI 2012 - Seventh ACM SIGPLAN Workshop on Types in Language Design and Implementation, Jan 2012, Philadelphia, United States
...
inria-00525874v1  Conference papers
Matthias PuechYann Régis-Gianas. Towards typed repositories of proofs
Mathematically Intelligent Proof Search - MIPS 2010, Jul 2010, Paris, France
inria-00629092v1  Conference papers
Yann Régis-GianasFrançois Pottier. A Hoare Logic for Call-by-Value Functional Programs
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⟩
...
hal-01890044v1  Conference papers
Yann Régis-GianasNicolas JeannerodRalf Treinen. Morbig: A Static Parser for POSIX Shell
SLE 2018 - ACM SIGPLAN International Conference on Software Language Engineering, Nov 2018, Boston, United States. ⟨10.1145/3276604.3276615⟩