Steel: proof-oriented programming in a dependently typed concurrent separation logic - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Proceedings of the ACM on Programming Languages Année : 2021

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

Résumé

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 et versions

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

Identifiants

Citer

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
74 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More