Rodolphe Lepigre

According to our database, Rodolphe Lepigre authored at least 14 papers between 2016 and 2022.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2022

BFF: foundational and automated verification of bitfield-manipulating programs.

Fengmin Zhu, Michael Sammler, Rodolphe Lepigre, Derek Dreyer, Deepak Garg

Proc. ACM Program. Lang., 2022

VIP: verifying real-world C idioms with integer-pointer casts.

Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, Peter Sewell

Proc. ACM Program. Lang., 2022

Islaris: verification of machine code against authoritative ISA semantics.

Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, Peter Sewell

Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

2021

RefinedC: automating the foundational verification of C code with refined ownership types.

Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg

Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

2020

The future is ours: prophecy variables in separation logic.

Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, Bart Jacobs

Proc. ACM Program. Lang., 2020

2019

Practical Subtyping for Curry-Style Languages.

Rodolphe Lepigre, Christophe Raffalli

ACM Trans. Program. Lang. Syst., 2019

PML 2 : Integrated Program Verification in ML.

Rodolphe Lepigre

CoRR, 2019

2018

Unboxing Mutually Recursive Type Definitions in OCaml.

Simon Colin, Rodolphe Lepigre, Gabriel Scherer

CoRR, 2018

Abstract Representation of Binders in OCaml using the Bindlib Library.

Rodolphe Lepigre, Christophe Raffalli

Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2018

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

PhD thesis, 2017

PML2: Integrated Program Verification in ML.

Rodolphe Lepigre

Proceedings of the 23rd International Conference on Types for Proofs and Programs, 2017

2016

Subtyping-Based Type-Checking for System F with Induction and Coinduction.

Rodolphe Lepigre, Christophe Raffalli

CoRR, 2016

A Realizability Model for a Semantical Value Restriction.

Rodolphe Lepigre

CoRR, 2016

A Classical Realizability Model for a Semantical Value Restriction.

Rodolphe Lepigre

Proceedings of the Programming Languages and Systems, 2016