Writing certifiably correct system software is still very labor-intensive, and current programming languages are not well suited for the task. Proof assistants work best on programs written in a high-level functional style, while operating systems need low-level control over the hardware. We present DeepSEA, a language which provides support for layered specification and abstraction refinement, effect encapsulation and composition, and full equational reasoning. A single DeepSEA program is automatically compiled into a certified ``layer'' consisting of a C program (which is then compiled into assembly by CompCert), a low-level functional Coq specification, and a formal (Coq) proof that the C program satisfies the specification. Multiple layers can be composed and interleaved with manual proofs to ascribe a high-level specification to a program by stepwise refinement. We evaluate the language by using it to reimplement two existing verified programs: a SHA-256 hash function and an OS kernel page table manager. This new style of programming language design can directly support the development of correct-by-construction system software.
Thu 24 Oct Times are displayed in time zone: Beirut change
11:00 - 11:22 Talk | DeepSEA: A Language for Certified System Software OOPSLA Vilhelm SjöbergYale University, Yuyang SangYale University, Shu-chun WengYale University, Zhong ShaoYale University DOI Pre-print | ||
11:22 - 11:45 Talk | Weakening WebAssembly OOPSLA Conrad WattUniversity of Cambridge, Andreas RossbergDfinity Stiftung, Jean Pichon-PharabodUniversity of Cambridge DOI | ||
11:45 - 12:07 Talk | Safer Smart Contract Programming with Scilla OOPSLA Ilya SergeyYale-NUS College and National University of Singapore, Vaivaswatha NagarajZilliqa Research, Jacob JohannsenZilliqa Research, Amrit KumarZilliqa Research, Anton TrunovZilliqa Research, Ken ChanZilliqa Research DOI Pre-print File Attached | ||
12:07 - 12:30 Talk | Scala Implicits Are Everywhere: A Large-Scale Study of the Use of Scala Implicits in the Wild OOPSLA Filip KřikavaCzech Technical University, Heather MillerCarnegie Mellon University, Jan VitekNortheastern University DOI Pre-print |