Pulse: Proof-Oriented Programming in Concurrent Separation Logic (Output C/Rust)
fstar-lang.org
1 thread
"Pulse is a new programming language embedded in F*, inheriting many of its features (notably, it is higher order and has dependent types), but with built-in support for programming with mutable state and concurrency, with specifications and proofs in Concurrent Separation Logic."