4
$\begingroup$

I am looking forward to learning Iris by myself, I have essential basic knowledge of Coq and logic but I don't know where to start. Logically, I looked into materials on the project website; the video tutorials are too brief, the lecture notes are almost incomplete without explanation, and to me "Iris from the ground up" paper requires lots of prior knowledge since I can't make sense of the syntax that is used there.
For someone who has no help what can be the best way to start learning Iris by himself?

$\endgroup$
3
  • 1
    $\begingroup$ I took the Semantics course (plv.mpi-sws.org/semantics-course). Of course, it's different when you attend a lecture (and have someone explain things to you) but I still find these lecture notes great. They have explanations, exercises, and a Coq development that also has exercises. $\endgroup$ Nov 25, 2023 at 15:45
  • $\begingroup$ @JoJoModding Sorry I ask this question here but I guess it would be dumb to open a thread for this. do you know what coding language the examples are in, (e.g fig 2 in Iris from ground up paper). it is not ML or any other language I'm familiar of. $\endgroup$ Dec 24, 2023 at 19:06
  • $\begingroup$ As usual in foundations, the programming language used does not really matter. And since real programming languages are often messy, you instead use a simplified version. The language used in the lecture notes is introduced in them. It is a version of System F + State + Recursive Types. You could also say it's pseudo code. If you know any functional language, you should have no trouble understanding it. $\endgroup$ Dec 25, 2023 at 10:53

1 Answer 1

6
$\begingroup$

Specifically for Iris, one useful resource is the POPL'21 tutorial. It remains terse for a self-studying newcomer however.

If you are not in a rush getting up to speed with Iris specifically, you may want to start with Arthur Chargueraud's book in the Software Foundation series.

It will introduce a number of concepts at a gentler pace, building up a foundational separation logic for a sequential language. Once you are confortable with this, scaling up to the concurrent and higher order fancy features of Iris may be easier.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.