Skip to Main content Skip to Navigation

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-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-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, 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-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
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⟩
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⟩