[GregarianChild]

I have another question, the abstract of your paper says that you "provide concurrency primitives in Rocq". But this is not really explained in the text. What are those "concurrency primitives"?

[joomy]

We mean Haskell-style software transactional memory (STM). We call it a primitive because it is not defined in Rocq itself; instead, it is only exposed to the Rocq programmer through an interface.

[GregarianChild]

Since the point of program extraction from a prover is correctness, I wonder what kind of assertions you prove for STM in Rocq.