Mechanized monadic equational reasoning for ML references (HOPE 2024)

Mon 2 - Sat 7 September 2024 Milan, Italy

Who

Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

Track

HOPE 2024

This program is tentative and subject to change.

Time Zone

The program is currently displayed in (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect 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

Mon 2 Sep 2024 16:30 - 17:00 at Orange 1 - Session 3

Abstract

We extend a Coq formalization of monadic equational reasoning with a monad to represent typed stores. This leads us to design an original equational theory, that we experimented on a number of examples. The examples themselves are generated from OCaml programs using an experimental compiler from OCaml to Coq, which targets the typed store monad.

File attachments

Extended abstract (friendly-hope.pdf)	247KiB

Reynald Affeldt

AIST

Jacques Garrigue

Nagoya University

Japan

Takafumi Saikawa