Write a Blog >>
Mon 20 Jan 2020 09:00 - 10:00 at Conde - Morning Keynote

Relational reasoning plays an important role in programming languages. For example, it is used to show that optimized versions of data structures behave the same as their non-optimized versions (contextual equivalence), to prove linearizability of concurrent data structures (contextual refinement), to prove correctness of program transformations (contextual refinement), and to prove that varying secret information does not lead to different behavior that can be observed by attackers (non-interference). In this talk, I will describe recent developments in concurrent separation logic (in the context of the Iris framework in the Coq proof assistant) that enable modular and mechanized relation reasoning in the context of rich languages with higher-order state and fine-grained concurrency.

Relational reasoning using concurrent separation logic (relational.pdf)1.31MiB

Mon 20 Jan
Times are displayed in time zone: Saskatchewan, Central America change

09:00 - 10:00
Morning KeynoteADSL at Conde
Relational reasoning using concurrent separation logic
A: Robbert KrebbersDelft University of Technology
Media Attached File Attached