POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Sat 20 Jan 2024 09:05 - 10:05 at Kelvin Lecture - Session 1

In recent years, there has been tremendous progress on developing program logics for verifying the correctness of programs in a rich and diverse array of languages. Thus far, however, such logics have assumed that programs are written entirely in a single programming language. In practice, this assumption rarely holds since programs are often composed of components written in different programming languages, which interact with one another via some kind of foreign function interface (FFI).

In this talk, I will present our first steps towards the goal of developing program logics for multi-language verification. Specifically, I will present Melocoton, a multi-language program verification system for reasoning about OCaml, C, and their interactions through the OCaml FFI. Melocoton consists of the first formal semantics of (a large subset of) the OCaml FFI—previously only described in prose in the OCaml manual—as well as the first program logic to reason about the interactions of program components written in OCaml and C.

Melocoton is fully mechanized in Coq on top of the Iris separation logic framework.

Slides (slides.pdf)3.26MiB

Sat 20 Jan

Displayed time zone: London change

09:00 - 10:30
Session 1CoqPL at Kelvin Lecture
Day opening

Melocoton: A Program Logic for Verified Interoperability Between OCaml and C (Invited Talk)
I: Armaël Guéneau Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria
File Attached
CertiCoq-Wasm: Verified compilation from Coq to WebAssembly
Wolfgang Meier , Jean Pichon-Pharabod Aarhus University, Bas Spitters Aarhus University
File Attached