The spirit of ghost code JC Filliātre, L Gondelman, A Paskevich Formal Methods in System Design 48, 152-174, 2016 | 97 | 2016 |

Finite sets in homotopy type theory D Frumin, H Geuvers, L Gondelman, N Weide Proceedings of the 7th ACM SIGPLAN International Conference on Certified …, 2018 | 27 | 2018 |

A pragmatic type system for deductive verification JC Filliātre, L Gondelman, A Paskevich | 23 | 2016 |

Distributed causal memory: modular specification and verification in higher-order distributed separation logic L Gondelman, SO Gregersen, A Nieto, A Timany, L Birkedal Proceedings of the ACM on Programming Languages 5 (POPL), 1-29, 2021 | 22 | 2021 |

Modular verification of op-based CRDTs in separation logic A Nieto, L Gondelman, A Reynaud, A Timany, L Birkedal Proceedings of the ACM on Programming Languages 6 (OOPSLA2), 1788-1816, 2022 | 13 | 2022 |

Trillium: Unifying refinement and higher-order distributed separation logic A Timany, SO Gregersen, L Stefanesco, L Gondelman, A Nieto, L Birkedal arXiv preprint arXiv:2109.07863, 27, 2021 | 13 | 2021 |

Verifying reliable network components in a distributed separation logic with dependent separation protocols L Gondelman, JK Hinrichsen, M Pereira, A Timany, L Birkedal Proceedings of the ACM on Programming Languages 7 (ICFP), 847-877, 2023 | 11 | 2023 |

The matrix reproved (verification pearl) M Clochard, L Gondelman, M Pereira Journal of Automated Reasoning 60, 365-383, 2018 | 11 | 2018 |

Semi-automated Reasoning About Non-determinism in C Expressions. D Frumin, L Gondelman, R Krebbers ESOP, 60-87, 2019 | 10 | 2019 |

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement A Timany, SO Gregersen, L Stefanesco, JK Hinrichsen, L Gondelman, ... Proceedings of the ACM on Programming Languages 8 (POPL), 241-272, 2024 | 5 | 2024 |

The matrix reproved (verification pearl) M Clochard, L Gondelman, M Pereira Verified Software. Theories, Tools, and Experiments: 8th International …, 2016 | 5 | 2016 |

Double WP: Vers une preuve automatique d'un compilateur M Clochard, L Gondelman Journées Francophones des Langages Applicatifs, 2015 | 4 | 2015 |

A toolchain to produce verified OCaml libraries JC Filliātre, L Gondelman, C Lourenēo, A Paskevich, M Pereira, ... | 3 | 2020 |

A Pragmatic Type System for Deductive Software Verification L Gondelman PhD thesis, Université Paris-Saclay, 2016 | 3 | 2016 |

A Toolchain to Produce Correct-by-Construction OCaml Programs JC FilliĀtRe, L Gondelman, A Paskevich, M Pereira, SM de Sousa Rapp. tech. artifact: https://www. lri. fr/~ mpereira/correct_ocaml. ova, 2018 | 2 | 2018 |

A benchmark for C program verification M van Eekelen, D Frumin, H Geuvers, L Gondelman, R Krebbers, ... arXiv preprint arXiv:1904.01009, 2019 | 1 | 2019 |

Modular Verification of State-Based CRDTs in Separation Logic AN Rodriguez, A Daby-Seesaram, L Gondelman, A Timany, L Birkedal Leibniz International Proceedings in Informatics (LIPIcs), 2023 | | 2023 |

Modular Verification of State-Based CRDTs in Separation Logic (Artifact) A Nieto, A Daby-Seesaram, L Gondelman, A Timany, L Birkedal Schloss-Dagstuhl-Leibniz Zentrum für Informatik, 2023 | | 2023 |

Modular Verification of State-Based CRDTs in Separation Logic A Nieto, A Daby-Seesaram, L Gondelman, A Timany, L Birkedal 37th European Conference on Object-Oriented Programming (ECOOP 2023), 2023 | | 2023 |

Semi-Automated Reasoning About Non-Determinism in C Expressions L Gondelman | | 2019 |