## Reading

For the seventh class, we will read **Interactive Proofs in a Higher-Order Concurrent Separation Logic** [PDF] [DOI] by Robbert Krebbers, Amin Timany, and Lars Brikedal.

This paper was a suggestion from my friend Tej Chajed. Tej recommended this paper because, in his words, "it's not search-style automation, but what it does do is implement a **high-level abstraction** (a more sophisticated logic) that happens to **look and feel similar to Coq's proof mode**. Using only the Iris Proof Mode, and maybe some lightweight extensions, we've been able to carry out pretty big proofs of program correctness. Some of it might be automated further but the [Iris Proof Mode] is really what makes things feasible because **each step is at such a high level of abstraction**."

In other words, what we have is a **cool embedded logic** inside of Coq that empowers proof engineers to use **powerful automation** to reason about programs inside of the embedded logic in a way that feels a lot like writing proofs outside of the embedding.

You can find a reading guide and the discussion questions below.

Please note that **this is due the morning before class**, so that we can discuss it in person. And **please install the artifact before Thursday's class**.