‹Programming› 2023
Mon 13 - Fri 17 March 2023 Tokyo, Japan
Mon 13 Mar 2023 16:25 - 16:50 at Faculty of Engineering Building 6, Seminar Room A - VIMPL Chair(s): Dimi Racordon

Value independence is enormously beneficial for reasoning about software systems at scale. These benefits carry over into the world of formal verification. Reasoning about programs algebraically is a simple affair in a proof assistant, whereas programs with unconstrained mutation necessitate much more complex techniques, such as Separation Logic, where invariants about memory safety, aliasing, and state changes must be established by manual proof.

Uniqueness type systems allow programs to be compiled to code that uses mutation for efficiency, while retaining a semantics that enjoys value independence for reasoning. The restrictions of these type systems, however, are often too onerous for realistic software. Thus, most uniqueness type systems include some “escape hatch” where the benefits of value independence for reasoning are lost, but the restrictions of uniqueness types are lifted. To formally verify a system with such mixed guarantees, the value independence guarantees from uniqueness types must be expressed in terms of imperative, mutable semantics. In other words, we ought to express value independence as an assertion in Separation Logic.

Mon 13 Mar

Displayed time zone: Osaka, Sapporo, Tokyo change

16:00 - 16:50
VIMPLMoreVMs / VIMPL at Faculty of Engineering Building 6, Seminar Room A
Chair(s): Dimi Racordon Northeastern University, USA
Lawvere: A categorical programming language with effectsVIMPL
James Haydon National Institute of Informatics, Japan
Uniqueness is SeparationVIMPL
Liam O'Connor University of Edinburgh, Pilar Selene Linares Arévalo University of Melbourne, Christine Rizkallah University of Melbourne