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
Interaction Trees: Representing Recursive and Impure Programs in Coq
Steve Zdancewic University of Pennsylvania
Connecting Separation Logic with First-Order Reasoning on Memory
William Mansky University of Illinois at Chicago, Wolf Honore
Typed Programming with Algebraic Effects (in terms of ambient values, functions, and control)
Daan Leijen Microsoft Research, USA