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?
$\begingroup$
$\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$– JoJoModdingCommented 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$– asha soroushpoorCommented 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$– JoJoModdingCommented Dec 25, 2023 at 10:53
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
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.
