Frédéric Besson -

Registered user since Mon 18 Sep 2023

Name:Frédéric Besson

Contributions

2027

PriSC

Committee Member in Program Committee within the PriSC 2027-track

RocqPL

Co-chair in Program Committee within the RocqPL-track

2026

LCTES

Author of Towards Verifiable System Code using a DSL Compiled to Efficient and Readable C Code within the LCTES 2026-track

SPLASH

Author of Formalizing the Linux eBPF Core ISA: A Mechanized Operational Semantics and Its Real-World Applications within the OOPSLA-track

RocqPL

Committee Member in Organizing Committee within the Rocq for Programming Languages 2026-track
Session Chair of Rocq Enhancements and Extensions (part of Rocq for Programming Languages 2026)

2025

PriSC

Author of BeePL: Correct-by-compilation kernel extensions within the PriSC 2025-track

2024

CPP

Author of PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams within the CPP 2024-track

2023

PPDP

Author of Type-directed Program Transformation for Constant-Time Enforcement within the PPDP 2023-track

2022

PriSC

Author of Type-directed Program Transformation for Constant-Time Enforcement within the PriSC 2022-track

2021

C&ESAR

Committee Member in Comité de programme / Program Committee

2020

PriSC

Committee Member in Program Committee within the Principles of Secure Compilation 2020-track

2019

ESOP

Author of Compiling Sandboxes: Formally Verified Software Fault Isolation within the ESOP 2019-track

2017

CoqPL

Author of ppsimpl: a reflexive Coq tactic for canonising goals within the CoqPL 2017-track

SCM

Presenter of Software Fault Isolation avec CompCert within the SCM-track