Skip to Main content Skip to Navigation


...
tel-02405839v1  Habilitation à diriger des recherches
Yann Regis-Gianas. About some Metamorphoses of Computer Programs
Programming Languages [cs.PL]. Université Paris Diderot, 2019
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⟩
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
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-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-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-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-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
...
tel-01890983v1  Theses
Guillaume Claret. Program in Coq
Programming Languages [cs.PL]. Université Paris Diderot - Paris 7, 2018. English
...
tel-01890508v1  Theses
Thibaut Girka. Differential program semantics
Programming Languages [cs.PL]. Université Paris Diderot, 2018. English
...
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-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
...
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-01962838v2  Conference papers
Cagdas BozmanBenjamin CanouRoberto Di CosmoPierrick CoudercLouis Gesbert et al.  Learn-OCaml : un assistant à l'enseignement d'OCaml
JFLA 2019 - Journées Francophones des Langages Applicatifs, Jan 2019, Les Rousses, France
...
inria-00525874v1  Conference papers
Matthias PuechYann Régis-Gianas. Towards typed repositories of proofs
Mathematically Intelligent Proof Search - MIPS 2010, Jul 2010, Paris, France