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.

@article{paperbot1140,
  title = {Steel: proof-oriented programming in a dependently typed concurrent separation logic},
  author = {Aymeric Fromherz and Aseem Rastogi and Nikhil Swamy and Sydney Gibson and Guido Martínez and Denis Merigoux and Tahina Ramananandro},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {5},
  number = {ICFP},
  year = {2021},
  doi = {10.1145/3473590}
}