tutorial-material.html

<!DOCTYPE html>
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta http-equiv="X-UA-Compatible" content="IE=edge">
    <meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">
    <meta name="description" content="">
    <meta name="author" content="">
    <meta name="referrer" content="origin-when-crossorigin">
    <link rel="icon" href="../../favicon.ico">

    <title>Iris Tutorial</title>

    <link rel="stylesheet" href="bootstrap.min.css" integrity="sha384-rbsA2VBKQhggwzxH7pPCaAqO46MgnOM80zW1RWuH61DGLwZJEdK2Kadq2F9CUG65" crossorigin="anonymous">

    <link rel="stylesheet" href="style.css" />

    <style>
        .lectures-table tr:nth-child(4n+1), .lectures-table tr:nth-child(4n+2) {
          background: #E0E0E0;
        }
    </style>

  </head>

  <body>
    <div class="bg-secondary py-5 mb-3 text-sm-center" style="--bs-bg-opacity : 0.1">
      <div class="container">
	    <h1 class="jumbotron-heading display-1">Iris Project</h1>

        <div>
	      <h2>Lecture Notes</h2>
        </div>
      </div>
    </div>

    <div class="container">

      <div>
        <p class="lead">
          Iris is a framework that can be used for reasoning about
          safety of concurrent programs, as the logic in logical
          relations, to reason about type-systems, data-abstraction
          etc.
          In case of questions, please contact us in our <a href="chat.html">chat room</a>.
        </p>
        <p class="lead">
          Below we provides notes from a lecture introducing to Iris.  The lecture notes have been used in an M.Sc. level course at
          Aarhus University. 

	      See the <a href="index.html">iris-project.org</a> page for
	      an overview of research that uses Iris one way or another.
      </div>

      <div class="container" style="margin-bottom:20px">
        <!--<div>
          <h2>Lecture Notes</h2>
        </div>-->

        <!--<div>
          <ul class="ref">-->
          <dl>
            <dt>Lecture Notes on Iris: Higher-Order Concurrent
              Separation Logic</dt>
            <dd>
              <div class="entry">
                Lars Birkedal, Aleš Bizjak<br/>
                <div class="buttons">
                  <a href="tutorial-pdfs/iris-lecture-notes.pdf"
		             class="btn btn-outline-primary btn-sm">.pdf</a>
		          <a
		            href="https://gitlab.mpi-sws.org/iris/examples/-/tree/master/theories/lecture_notes"
		            class="btn btn-outline-primary btn-sm">Rocq example files</a>
		          <a
		            href="https://github.com/logsem/iris-lecture-notes/"
		            class="btn btn-outline-primary btn-sm">TeX source files</a>
                </div>
              </div>
            </dd>
          </dl>
	  <!--    </ul>
          </div>-->
	      
          <div>
	        <h4>Course Plan with Slides</h4>
          </div>

          
          <table class="text-nowrap table table-bordered border-secondary">
            <thead>
              <tr>
                <th>Week</th>
                <th>Day</th>
                <th>Lecture</th>
                <th>Literature</th>
                <th>Slides</th>
                <th>Hand-in Exercises</th>
              </tr>
            </thead>
            <tbody class="lectures-table">
              <tr>
                <td rowspan="2" class="text-center align-middle">1</td>
                <td>Day 1</td>
                <td><strong>Intro + Operational Semantics</strong></td>
                <td>ILN Sec. 1+2</td>
                <td><a href="tutorial-pdfs/lecture1-intro-opsem.pdf">lecture1</a></td>
                <td></td>
              </tr>
              <tr>
                <td>Day 2</td>
                <td><strong>Basic Logic of Resources</strong></td>
                <td>ILN Sec. 3</td>
                <td><a href="tutorial-pdfs/lecture2-basic-logic-of-resources.pdf">lecture2</a></td>
                <td>ILN Ex. 3.2</td>
              </tr>
              <tr>
                <td rowspan="2" class="text-center align-middle">2</td>
                <td>Day 1</td>
                <td><strong>Basic Separation Logic: Hoare Triples</strong></td>
                <td>ILN Sec. 4.0</td>
                <td><a href="tutorial-pdfs/lecture3-basic-hoare-triples.pdf">lecture3</a></td>
                <td></td>
              </tr>
              <tr>
                <td>Day 2</td>
                <td><strong>Basic Separation Logic: Proving
                    Pointer Programs</strong></td>
                <td>ILN Sec. 4.1</td>
                <td><a href="tutorial-pdfs/lecture4-lists.pdf">lecture4</a></td>
                <td>ILN Ex. 4.1, 4.2, 4.5, 4.11, 4.21</td>
              </tr>
              <tr>
                <td rowspan="2" class="text-center align-middle">3</td>
                <td>Day 1</td>
                <td><strong>Basic Separation Logic: Abstract
                    Data Types</strong></td>
                <td>ILN Sec. 4.2</td>
                <td><a href="tutorial-pdfs/lecture5-adt-styles.pdf">lecture5</a></td>
                <td></td>
              </tr>
              <tr>
                <td>Day 2</td>
                <td><strong>Case Study: foldr</strong></td>
                <td>ILN Sec. 4.3</td>
                <td><a href="tutorial-pdfs/lecture6-foldr.pdf">lecture6</a></td>
                <td>ILN Ex. 4.29, 4.34</td>
              </tr>
              <tr>
                <td rowspan="2" class="text-center align-middle">4</td>
                <td>Day 1</td>
                <td><strong>Later Modality</strong></td>
                <td>ILN Sec. 5</td>
                <td><a href="tutorial-pdfs/lecture7-later.pdf">lecture7</a></td>
                <td></td>
              </tr>
              <tr>
                <td>Day 2</td>
                <td><strong>Always Modality</strong></td>
                <td>ILN Sec. 6</td>
                <td><a href="tutorial-pdfs/lecture8-persistent.pdf">lecture8</a></td>
                <td>ILN Ex. 5.3, 6.2 item (1) (2) and (4)</td>
              </tr>
              <tr>
                <td rowspan="2" class="text-center align-middle">5</td>
                <td>Day 1</td>
                <td><strong>Concurrency: par + invariants</strong></td>
                <td>ILN Sec. 7.1 + 7.2</td>
                <td><a href="tutorial-pdfs/lecture9-invariants.pdf">lecture9</a></td>
                <td></td>
              </tr>
              <tr>
                <td>Day 2</td>
                <td><strong>Concurrency: ghost state</strong></td>
                <td>ILN Sec. 7.4 + 7.5</td>
                <td><a href="tutorial-pdfs/lecture10-ghost-state.pdf">lecture10</a></td>
                <td>ILN Ex. 7.6, 7.24 item (3), 7.29, 7.32 (the first triple)</td>
              </tr>
              <tr>
                <td rowspan="2" class="text-center align-middle">6</td>
                <td>Day 1</td>
                <td><strong>Concurrency: Case Study: spin lock + concurrent bag</strong></td>
                <td>ILN Sec. 7.6</td>
                <td><a href="tutorial-pdfs/lecture11-cas-spin-lock.pdf">lecture11</a></td>
                <td></td>
              </tr>
              <tr>
                <td>Day 2</td>
                <td><strong>Concurrency: Case Study: counter modules</strong></td>
                <td>ILN Sec. 7.7</td>
                <td><a href="tutorial-pdfs/lecture12-counter-modules.pdf">lecture12</a></td>
                <td>ILN Ex. 7.37, 7.42.</td>
              </tr>
              <tr>
                <td rowspan="2" class="text-center align-middle">7</td>
                <td>Day 1</td>
                <td><strong>Weakest preconditions and fancy update modality</strong></td>
                <td>ILN Sec. 8.1 + 8.2</td>
                <td><a href="tutorial-pdfs/lecture13-wp-fancy-update-modality.pdf">lecture13</a></td>
                <td></td>
              </tr>
              <tr>
                <td>Day 2</td>
                <td><strong>Concurrency: Case Study: concurrent stack with helping</strong></td>
                <td>ILN Sec. 10</td>
                <td><a href="tutorial-pdfs/lecture14-stacks-with-helping.pdf">lecture14</a></td>
                <td>ILN Ex. 7.43 (the one for incr), 7.47, 7.49 (the two specs for read).</td>
              </tr>
            </tbody>
          </table>
        </div>
      </div>
      
      <!--<div class="container" style="margin-bottom: 20px;">
        <div>
          <h2>POPL'18 Tutorial</h2>
        </div>

        <div>
          <ul class="ref">
            <dt>Iris - A Modular Foundation for Higher-Order Concurrent Separation Logic</dt>
            <dd>
              <div class="entry">
                Jacques-Henri Jourdan, Robbert Krebbers<br/>
                <div class="buttons">
                  <a href="https://gitlab.mpi-sws.org/iris/tutorial-popl18"
		             class="btn btn-outline-primary btn-sm">Tutorial material</a>
                </div>
            </dd>
	      </ul>
          </div>
        </div>
      </div>-->

  </body>
</html>