Follow
Rodolphe Lepigre
Rodolphe Lepigre
Verified email at mpi-sws.org - Homepage
Title
Cited by
Cited by
Year
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
832021
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
692019
A classical realizability model for a semantical value restriction
R Lepigre
Programming Languages and Systems: 25th European Symposium on Programming …, 2016
302016
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
222022
Practical subtyping for Curry-style languages
R Lepigre, C Raffalli
ACM Transactions on Programming Languages and Systems (TOPLAS) 41 (1), 1-58, 2019
18*2019
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
12*2017
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
82022
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, ...
72020
Unboxing Mutually Recursive Type Definitions in OCaml
S Colin, R Lepigre, G Scherer
arXiv preprint arXiv:1811.02300, 2018
72018
Abstract representation of binders in ocaml using the bindlib library
R Lepigre, C Raffalli
arXiv preprint arXiv:1807.01872, 2018
72018
PML 2: Integrated Program Verification in ML
R Lepigre
arXiv preprint arXiv:1901.03208, 2019
22019
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
12022
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
The system can't perform the operation now. Try again later.
Articles 1–18