This program is tentative and subject to change.

Sat 22 Jan 2022 17:05 - 17:30 at Independence - Secure systems Chair(s): Arthur Azevedo de Amorim

In this extended abstract, we propose effect-oblivious equivalence, an equivalence relation for effectful programs that holds regardless of the implementation details of effects. Effect-oblivious equivalence is useful for reasoning about optimizations of programs whose effect implementations are unknown at the compile time, e.g., when the program can interact with different external environment at run time, or when the effect handlers are implemented separately, etc. When the effect implementations are known, effect-oblivious equivalence might still be useful for reasoning about optimizations that do not rely on assumptions over the effect implementations, e.g., the pure parts of a program.

We show that effect-oblivious equivalence in many programming languages can be encoded using general laws of classes of functors from Haskell. Furthermore, we can inherit the effect-oblivious equivalence properties if we use free structures of a suitable class of functors to model the semantics. We show that these free structures include the commonly used free monads, but also other structures like free applicative functors.

Effect-Oblivious Equivalence (Extended Abstract) (extended-abstract.pdf)391KiB

This program is tentative and subject to change.

Sat 22 Jan

Displayed time zone: Eastern Time (US & Canada) change

16:40 - 17:55
Secure systemsPriSC at Independence
Chair(s): Arthur Azevedo de Amorim Boston University, USA
16:40
25m
Talk
A CompCert backend with symbolic encryption
PriSC
Paolo Torrini INRIA, Sylvain Boulmé Grenoble Alps University / CNRS / Grenoble INP / VERIMAG
17:05
25m
Talk
Effect-Oblivious Equivalence
PriSC
Yao Li University of Pennsylvania, Stephanie Weirich University of Pennsylvania
Pre-print File Attached
17:30
25m
Talk
The Supervisionary proof-checking kernel, or: a work-in-progress toward proof-generating code
PriSC
Dominic Mulligan Arm Research, Nick Spinale Arm Research
Hide past events