Issues

• Example 8.7: errors in proof

  logsem/iris-lecture-notes#19 · Filter by author mildsunrise opened on Sep 28, 2026

• Exercise 8.2: lacking rule for CAS

  logsem/iris-lecture-notes#18 · Filter by author mildsunrise opened on Sep 25, 2026

• Consider if it makes sense to use FAA instead of a CAS-loop in the authoritative RA counter example.

  logsem/iris-lecture-notes#12 · Filter by author jihgfee opened on Nov 21, 2022

• Lack of consistency between notations of equality/assignment

  logsem/iris-lecture-notes#11 · Filter by author jihgfee opened on Nov 17, 2022

• Identify and fix discrepancies between different notation

  logsem/iris-lecture-notes#10 · Filter by author jihgfee opened on Nov 8, 2022

• Modular Concurrent Counter Module: The RA of the ILN does not match the one in Coq

  logsem/iris-lecture-notes#7 · Filter by author jihgfee opened on Nov 1, 2022

• The fancy view shift is defined with a regular implication => but used wands in the Iris technical documentation -*

  logsem/iris-lecture-notes#5 · Filter by author jihgfee opened on Oct 26, 2022

• One of the bupd rules in Exercise 8.24 is not named, and not in the appendix

  logsem/iris-lecture-notes#4 · Filter by author jihgfee opened on Oct 26, 2022

• S is persistent is not formally defined

  logsem/iris-lecture-notes#2 · Filter by author jihgfee opened on Oct 14, 2022

• Improve the section on authoritative resource algebras

  logsem/iris-lecture-notes#1 · Filter by author jihgfee opened on Oct 14, 2022