Contact: (λ x y . “email@example.com”) “glen” “mevel”.
PhD student (2018–), team Gallium, Inria Paris, France.
With my advisors François Pottier and Jacques‐Henri Jourdan, we aim at establishing a program logic for proving correctness of Multicore OCaml programs. For that, we are using the Coq proof assistant and the Iris separation logic.
Research interests: functional programming, proof of programs, multicore programming, type systems…
We present a machine-checked extension of the program logic Iris with time credits and time receipts, two dual means of reasoning about time. Whereas time credits are used to establish an upper bound on a program's execution time, time receipts can be used to establish a lower bound. More strikingly, time receipts can be used to prove that certain undesirable events — such as integer overflows — cannot occur until a very long time has elapsed. We present several machine-checked applications of time credits and time receipts, including an application where both concepts are exploited.I gave a companion talk at ESOP 2019. [PDF of the talk] The Coq proofs are available here.