| RefinedC: automating the foundational verification of C code with refined ownership types M Sammler, R Lepigre, R Krebbers, K Memarian, D Dreyer, D Garg Proceedings of the 42nd ACM SIGPLAN International Conference on Programming …, 2021 | 109 | 2021 |
| The future is ours: prophecy variables in separation logic R Jung, R Lepigre, G Parthasarathy, M Rapoport, A Timany, D Dreyer, ... Proceedings of the ACM on Programming Languages 4 (POPL), 1-32, 2019 | 79 | 2019 |
| A classical realizability model for a semantical value restriction R Lepigre Programming Languages and Systems: 25th European Symposium on Programming …, 2016 | 31 | 2016 |
| Islaris: verification of machine code against authoritative ISA semantics M Sammler, A Hammond, R Lepigre, B Campbell, J Pichon-Pharabod, ... Proceedings of the 43rd ACM SIGPLAN International Conference on Programming …, 2022 | 30 | 2022 |
| Practical subtyping for Curry-style languages R Lepigre, C Raffalli ACM Transactions on Programming Languages and Systems (TOPLAS) 41 (1), 1-58, 2019 | 19* | 2019 |
| VIP: verifying real-world C idioms with integer-pointer casts R Lepigre, M Sammler, K Memarian, R Krebbers, D Dreyer, P Sewell Proceedings of the ACM on Programming Languages 6 (POPL), 1-32, 2022 | 15 | 2022 |
| Semantics and Implementation of an Extension of ML for Proving Programs.(Sémantique et Implantation d'une Extension de ML pour la Preuve de Programmes). R Lepigre Grenoble Alpes University, France, 2017 | 13* | 2017 |
| The future is ours: Prophecy variables in separation logic. PACMPL 4, POPL (2020), 45: 1–45: 32 R Jung, R Lepigre, G Parthasarathy, M Rapoport, A Timany, D Dreyer, ... | 11 | 2020 |
| Unboxing Mutually Recursive Type Definitions in OCaml S Colin, R Lepigre, G Scherer arXiv preprint arXiv:1811.02300, 2018 | 10 | 2018 |
| Abstract representation of binders in ocaml using the bindlib library R Lepigre, C Raffalli arXiv preprint arXiv:1807.01872, 2018 | 7 | 2018 |
| BFF: Foundational and automated verification of bitfield-manipulating programs F Zhu, M Sammler, R Lepigre, D Dreyer, D Garg Proceedings of the ACM on Programming Languages 6 (OOPSLA2), 1613-1638, 2022 | 2 | 2022 |
| PML 2: Integrated Program Verification in ML R Lepigre arXiv preprint arXiv:1901.03208, 2019 | 2 | 2019 |
| Artifact and Appendix of" RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types" M Sammler, R Lepigre, RJ Krebbers, K Memarian, D Dreyer, D Garg Zenodo, 2021 | | 2021 |
| Artifact and Appendix of" VIP: Verifying Real-World C Idioms with Integer-Pointer Casts" R Lepigre, M Sammler, K Memarian, R Krebbers, D Dreyer, P Sewell Zenodo, 2021 | | 2021 |
| A Classical Realizability Interpretation of Judgement Testing R Lepigre ENS Lyon, 2013 | | 2013 |
| Internship report Testing judgements of type theory Chalmers Tekniska Högskola, Göteborg R Lepigre | | 2012 |
| Theory and Demo of PML2: Proving Programs in ML R Lepigre | | |
| Mêler combinateurs, continuations et EBNF pour une analyse syntaxique efficace en OCaml R Lepigre, C Raffalli | | |
Derek DreyerMax Planck Institute for Software Systems (MPI-SWS), Saarland Informatics CampusEmail verificata su mpi-sws.org