Sat 22 Jun 2019 16:20 - 16:45 at 106B - Interaction Trees and Algebraic Effects I Chair(s): Andrew Appel

The Verified Software Toolchain (VST) gives us a powerful tool for proving correctness of C programs. With the recent addition of mechanisms for external state, we can even reason about the behavior of programs that communicate with the outside world, for instance via network sockets or console I/O. But the implementations of these communication functions cannot be verified with VST: they involve the state of the operating system and interactions with device drivers, and break the usual single-program, single-memory abstraction of user-level programs. In this talk, we will present work on connecting VST proofs to system call implementations in CertiKOS, the verified operating system, which uses a different approach to verifying (kernel-level) C code. Such a connection must bridge the gap between VST’s step-indexed, ownership-annotated model of memory and CertiKOS’s more concrete representation, as well as establishing a common language for talking about communication events across user programs and the OS.

Sat 22 Jun

Displayed time zone: Tijuana, Baja California change

16:00 - 17:30
Interaction Trees and Algebraic Effects IDeepSpec at 106B
Chair(s): Andrew Appel Princeton
16:00
20m
Talk
Interaction Trees: Representing Recursive and Impure Programs in Coq
DeepSpec
Steve Zdancewic University of Pennsylvania
16:20
25m
Talk
Connecting Separation Logic with First-Order Reasoning on Memory
DeepSpec
William Mansky University of Illinois at Chicago, Wolf Honore
16:45
45m
Talk
Typed Programming with Algebraic Effects (in terms of ambient values, functions, and control)
DeepSpec
Daan Leijen Microsoft Research, USA