Steel: proof-oriented programming in a dependently typed concurrent separation logic - Archive ouverte HAL Access content directly
Journal Articles Proceedings of the ACM on Programming Languages Year : 2021

Steel: proof-oriented programming in a dependently typed concurrent separation logic

(1) , (2) , (3) , (1) , (4) , (5) , (3)
1
2
3
4
5

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.

Dates and versions

hal-03466397 , version 1 (05-12-2021)

Identifiers

Cite

Aymeric Fromherz, Aseem Rastogi, Nikhil Swamy, Sydney Gibson, Guido Martínez, et al.. Steel: proof-oriented programming in a dependently typed concurrent separation logic. Proceedings of the ACM on Programming Languages, 2021, 5 (ICFP), pp.1-30. ⟨10.1145/3473590⟩. ⟨hal-03466397⟩

Collections

INRIA INRIA2
47 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More