Rodolphe Lepigre

ORCID

Publication Activity (10 Years)

Years Active: 2016-2022
Publications (10 Years): 13

Top Venues

CoRR

Proc. ACM Program. Lang.

PLDI

LFMTP@FSCD

Grenoble Alpes University, France (PHD)

Education History

Grenoble Alpes University, France

PHD

Publications

Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, Peter Sewell
VIP: verifying real-world C idioms with integer-pointer casts. Proc. ACM Program. Lang. 6 (POPL) (2022)
Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, Peter Sewell
Islaris: verification of machine code against authoritative ISA semantics. PLDI (2022)
Fengmin Zhu, Michael Sammler, Rodolphe Lepigre, Derek Dreyer, Deepak Garg
BFF: foundational and automated verification of bitfield-manipulating programs. Proc. ACM Program. Lang. 6 (OOPSLA2) (2022)
Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg
RefinedC: automating the foundational verification of C code with refined ownership types. PLDI (2021)
Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, Bart Jacobs
The future is ours: prophecy variables in separation logic. Proc. ACM Program. Lang. 4 (POPL) (2020)
Rodolphe Lepigre, Christophe Raffalli
Practical Subtyping for Curry-Style Languages. ACM Trans. Program. Lang. Syst. 41 (1) (2019)
Rodolphe Lepigre
PML 2 : Integrated Program Verification in ML. CoRR (2019)
Simon Colin, Rodolphe Lepigre, Gabriel Scherer
Unboxing Mutually Recursive Type Definitions in OCaml. CoRR (2018)
Rodolphe Lepigre, Christophe Raffalli
Abstract Representation of Binders in OCaml using the Bindlib Library. LFMTP@FSCD (2018)
Rodolphe Lepigre
PML2: Integrated Program Verification in ML. TYPES (2017)
Rodolphe Lepigre
A Realizability Model for a Semantical Value Restriction. CoRR (2016)
Rodolphe Lepigre, Christophe Raffalli
Subtyping-Based Type-Checking for System F with Induction and Coinduction. CoRR (2016)
Rodolphe Lepigre
A Classical Realizability Model for a Semantical Value Restriction. ESOP (2016)

Rodolphe Lepigre.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Rodolphe Lepigre