Steel

Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic

Aymeric Fromherz, Carnegie Mellon University, USA
Aseem Rastogi, Microsoft Research, India
Nikhil Swamy, Microsoft Research, USA
Sydney Gibson, Carnegie Mellon University, USA
Guido Martínez, CIFASIS-CONICET, Argentina
Denis Merigoux, Inria Paris, France
Tahina Ramananandro, Microsoft Research, USA

Presented In The
26th ACM SIGPLAN International Conference on Functional Programming

Abstract

Steel is a language for developing and proving concurrent programs embedded in F⭑, a dependently typed programming language and proof assistant. Based on SteelCore, a concurrent separation logic (CSL) formalized in F⭑, our work focuses on exposing the proof rules of the logic in a form that enables programs and proofs to be effectively co-developed.

Our main contributions include a new formulation of a Hoare logic of quintuples involving both separation logic and first-order logic, enabling efficient verification condition (VC) generation and proof discharge using a combination of tactics and SMT solving. We relate the VCs produced by our quintuple system to solving a system of associativity-commutativity (AC) unification constraints and develop tactics to (partially) solve these constraints using AC-matching modulo SMT-dischargeable equations.

Our system is fully mechanized and implemented in F⭑. We evaluate it by developing several verified programs and libraries, including various sequential and concurrent linked data structures, proof libraries, and a library for 2-party session types. Our experience leads us to conclude that our system enables a mixture of automated and interactive proof, making it productive to build programs foundationally verified against a highly expressive, state-of-the-art CSL.

• Paper (PDF)
• ICFP talk video
• Published version (in ACM DL, open access)
• Evaluated software artifact (in ACM DL)
• Steel on GitHub
• F⭑ on GitHub
• F⭑ project page