Steel: proof-oriented programming in a dependently typed concurrent separation logic
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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Aug 19, 2021
- Source ID
- 10.1145/3473590
Entities
People
- Aseem Rastogi
- Aymeric Fromherz
- Denis Merigoux
- Guido Martínez
- Nikhil Swamy
- Sydney Gibson
- Tahina Ramananandro
Organizations
- Alfred P. Sloan Foundation
- Carnegie Mellon University
- European Research Council
- Institut National de Recherche en Informatique et en Automatique
- Intel Corporation
- Microsoft
- National Science Foundation
- Office of Naval Research