Rodolphe Lepigre

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