CertiCoq-Wasm: Verified compilation from Coq to WebAssembly (CoqPL 2024 - The Tenth International Workshop on Coq for Programming Languages)

Sun 14 - Sat 20 January 2024 London, United Kingdom

Who

Wolfgang Meier, Jean Pichon-Pharabod, Bas Spitters

Track

CoqPL 2024

Time Zone

The program is currently displayed in (GMT) London.

Use conference time zone: (GMT) LondonSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Sat 20 Jan 2024 10:05 - 10:30 at Kelvin Lecture - Session 1

Abstract

We describe CertiCoq-Wasm, a verified compiler from the Gallina programming language of the Coq theorem prover to WebAssembly. CertiCoq-Wasm is mechanised with respect to the WasmCert-Coq formalisation of the WebAssembly 1.0 standard, and produces WebAssembly programs with reasonable performance. Internally, CertiCoq-Wasm is based on the CertiCoq pipeline, and diverges only at the lowering from its minimal lambda calculus in administrative normal form.

File attachments

certicoq-wasm:coqpl2024.pdf (coqpl24-final3.pdf)	416KiB
Slides (certicoq-wasm-slides.pdf)	312KiB

Wolfgang Meier

Jean Pichon-Pharabod

Aarhus University

Denmark

Bas Spitters