ITree home page / bibliography

.gitignore

@@ -36,7 +36,7 @@ tutorial/_CoqProject
 _CoqPath
 lib/
 html/
-doc
+gh-pages
 coqdocjs*
 
 tests/extraction/*.ml
@@ -50,3 +50,5 @@ tutorial/imp_test.mli
 *.native
 
 *.install
+
+doc/index.html

DEV.md

@@ -103,24 +103,24 @@ CSS and JS to coqdoc's output.
 #### 3. Updating Github pages
 
 The documentation is stored in the `gh-pages` branch.
-The recommended setup is to create a fresh clone in the `doc` directory.
+The recommended setup is to create a fresh clone in the `gh-pages` directory.
 
 ```
-git clone -b gh-pages git@github.com:DeepSpec/InteractionTrees doc
+git clone -b gh-pages git@github.com:DeepSpec/InteractionTrees gh-pages
 ```
 
 There is a script in that branch to update the documentation.
 
 ```
-cd doc
+cd gh-pages
 sh ./update.sh
 git add -u
 git commit -m "Update"
 ```
 
 It will run "make html" in the parent directory and move the output where it
-should go, in `doc/docs/master`.
-Past releases are maintained in `doc/docs/$VERSION`.
+should go, in `gh-pages/docs/master`.
+Past releases are maintained in `gh-pages/docs/$VERSION`.
 
 ## Library internal organization
 

doc/assets/style.css

@@ -0,0 +1,106 @@
+@import url('https://fonts.googleapis.com/css2?family=Noto+Sans&family=Noto+Serif&display=swap');
+
+html {
+  font-family: 'Noto Sans', sans-serif;
+}
+
+h1, h2 {
+  font-family: 'Noto Serif', serif;
+  text-align: center;
+}
+
+.github::after {
+  display: inline-flex;
+  content: '';
+  vertical-align: middle;
+  margin-left: 0.5em;
+  background-image: url('github.svg');
+  background-size: 1.3em 1.3em;
+  height: 1.3em;
+  width: 1.3em;
+}
+
+.pub-title > a {
+  text-decoration: none;
+  font-weight: bold;
+}
+
+.pub-paper::after {
+  vertical-align: middle;
+  margin-left: 0.3em;
+}
+
+@media only screen and (min-width: 768px) {
+  .level-2 { margin-left: 2em; }
+}
+
+li {
+  margin-bottom: 1em;
+}
+
+.item-paper::marker {
+  content: '🖹  ';
+  font-size: 1.2em;
+}
+
+input[name="tag-select"] {
+  display: none;
+}
+
+input + label {
+  cursor: pointer;
+}
+
+@keyframes targetted {
+  from { background-color: gold; }
+}
+
+.pill:target {
+  animation-name: targetted !important;
+  animation-duration: 2s;
+}
+
+.pill {
+  display: inline-block;
+  border: 1px solid ;
+  border-radius: 0.8em;
+  padding: 0.1em 0.5em;
+  text-decoration: none;
+}
+
+.pill.notag { border: dotted; color: gray; }
+.pill.tag-coq { color: red; }
+.pill.tag-isabelle { color: peru; }
+.pill.tag-vst { color: green; }
+.pill.tag-monads { color: blueviolet; }
+.pill.tag-coinduction { color: teal; }
+.pill.tag-testing { color: slateblue; }
+.pill.tag-concurrency { color: deeppink; }
+.pill.tag-plclub { color: dodgerblue; }
+
+.pub-conf + .pill { margin-left: 0.5em; }
+.pub-conf ~ .pill { margin-top: 0.2em; }
+
+input:checked + .pill.tag-coq, input#tag-coq:checked ~ ul .pill.tag-coq { background-color: red; border-color: red; color: white; }
+input:checked + .pill.tag-isabelle, input#tag-isabelle:checked ~ ul .pill.tag-isabelle { background-color: peru; border-color: peru; color: white; }
+input:checked + .pill.tag-vst, input#tag-vst:checked ~ ul .pill.tag-vst { background-color: green; border-color: green; color: white; }
+input:checked + .pill.tag-monads, input#tag-monads:checked ~ ul .pill.tag-monads { background-color: blueviolet; border-color: blueviolet; color: white; }
+input:checked + .pill.tag-coinduction, input#tag-coinduction:checked ~ ul .pill.tag-coinduction { background-color: teal; border-color: teal; color: white; }
+input:checked + .pill.tag-testing, input#tag-testing:checked ~ ul .pill.tag-testing { background-color: slateblue; border-color: slateblue; color: white; }
+input:checked + .pill.tag-concurrency, input#tag-concurrency:checked ~ ul .pill.tag-concurrency { background-color: deeppink; border-color: deeppink; color: white; }
+input:checked + .pill.tag-plclub, input#tag-plclub:checked ~ ul .pill.tag-plclub { background-color: dodgerblue; border-color: dodgerblue; color: white; }
+
+input.tag-select:checked ~ ul > li {
+  display: none;
+}
+
+input#tag-coq:checked ~ ul > li.tag-coq,
+input#tag-isabelle:checked ~ ul > li.tag-isabelle,
+input#tag-vst:checked ~ ul > li.tag-vst,
+input#tag-monads:checked ~ ul > li.tag-monads,
+input#tag-coinduction:checked ~ ul > li.tag-coinduction,
+input#tag-testing:checked ~ ul > li.tag-testing,
+input#tag-concurrency:checked ~ ul > li.tag-concurrency,
+input#tag-plclub:checked ~ ul > li.tag-plclub {
+  display: revert;
+}

doc/index.html.jingoo

@@ -0,0 +1,55 @@
+<!doctype html>
+<html lang="en">
+<head>
+  <meta charset="utf-8">
+  <meta name="viewport" content="width=device-width,initial-scale=1">
+  <title>Interaction Trees</title>
+  <meta name="description" content="Homepage of the Interaction Trees project">
+  <!-- TODO: OpenGraph -->
+  <!-- TODO: favicon -->
+  <link rel="stylesheet" href="assets/style.css">
+</head>
+<body>
+<h1 id="interaction-trees">Interaction Trees</h1>
+<h2 id="source-code">Library</h2>
+<div class="level-2">
+<h3>
+<a class="github" href="https://github.com/DeepSpec/InteractionTrees">Source Code</a>
+</h3>
+<h3>Documentation</h3>
+<ul class="doclist">
+  <li><a href="./master/toc.html">Development version (master branch)</a></li>
+  <li><a href="./5.0.0/toc.html">Version 5.0.0</a></li>
+</ul>
+<!-- TODO: Features -->
+<!-- TODO: Connected projects (coq-itree-io, coq-ffi) -->
+</div>
+<h2 id="the-interaction-trees-academic-universe">The Interaction Trees Academic Universe</h2>
+<div class="level-2">
+<p>List of publications about or closely related to Interaction Trees.</p>
+<input type="radio" id="notag" name="tag-select"><label for="notag" class="pill notag">show all</label>
+{% for tag in ["coq", "isabelle", "vst", "monads", "coinduction", "testing", "concurrency", "plclub"] %}
+<input type="radio" id="tag-{{tag}}" name="tag-select" class="tag-select">
+<label for="tag-{{tag}}" id="label-{{tag}}" class="pill tag-{{tag}}" title="woop">{{ tag }}</label>
+{% endfor %}
+{%- include "pubs.jingoo" -%}
+{% for y in contents -%}
+<h3>{{ y.year }}</h3>
+<ul>
+{% for pub in y.pubs -%}
+<li class="item-paper{% for tag in pub.tags %} tag-{{ tag }}{% endfor %}">
+  <div class="pub-title"><a href="{{ pub.url }}">{{ pub.title }}</a></div>
+  <div class="pub-authors">by {{ pub.authors }}</div>
+  <div>
+    <span class="pub-conf">{{ pub.conf }}</span>
+    {%- for tag in pub.tags %}
+    <a class="pill tag tag-{{tag}}" href="#label-{{tag}}">{{ tag }}</a>
+    {%- endfor -%}
+  </div>
+</li>
+{% endfor %}
+</ul>
+{% endfor %}
+</div>
+</body>
+</html>

doc/pubs.jingoo

@@ -0,0 +1,114 @@
+{%- set contents = [
+  { year: 2019
+  , pubs: [
+      { title: "From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server"
+      , authors: "Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, Steve Zdancewic"
+      , conf: "CPP 2019"
+      , url: "https://dl.acm.org/doi/10.1145/3293880.3294106"
+      , tags: ["coq", "vst", "testing", "plclub"]
+      }
+    ]
+  },
+  { year: 2020
+  , pubs: [
+      { title: "Interaction Trees: Representing Recursive and Impure Programs in Coq"
+      , authors: "Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic"
+      , conf: "POPL 2020"
+      , url: "https://dl.acm.org/doi/10.1145/3371119"
+      , tags: ["coq", "monads", "coinduction", "plclub"]
+      },
+      { title: "An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction"
+      , authors: "Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic"
+      , conf: "CPP 2020"
+      , url: "https://dl.acm.org/doi/abs/10.1145/3372885.3373813"
+      , tags: ["coq", "coinduction", "plclub"]
+      },
+      { title: "Connecting Higher-Order Separation Logic to a First-Order Outside World"
+      , authors: "William Mansky, Wolf Honoré, Andrew W. Appel"
+      , conf: "ESOP 2020"
+      , url: "https://link.springer.com/chapter/10.1007/978-3-030-44914-8_16"
+      , tags: ["coq", "vst"]
+      }
+    ]
+  },
+  { year: 2021
+  , pubs: [
+      { title: "Dijkstra Monads Forever: Termination-Sensitive Specifications for Interaction Trees"
+      , authors: "Lucas Silver, Steve Zdancewic"
+      , conf: "POPL 2021"
+      , url: "https://dl.acm.org/doi/10.1145/3434307"
+      , tags: ["coq", "monads", "coinduction", "plclub"]
+      },
+      { title: "Model-based Testing of Networked Applications"
+      , authors: "Yishuai Li, Benjamin C. Pierce, Steve Zdancewic"
+      , conf: "ISSTA 2021"
+      , url: "https://dl.acm.org/doi/abs/10.1145/3460319.3464798"
+      , tags: ["coq", "testing", "plclub"]
+      },
+      { title: "Verifying an HTTP Key-Value Server with Interaction Trees and VST"
+      , authors: "Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, William Mansky, Benjamin C. Pierce, Steve Zdancewic"
+      , conf: "ITP 2021"
+      , url: "https://drops.dagstuhl.de/opus/volltexte/2021/13927/"
+      , tags: ["coq", "vst", "testing", "plclub"]
+      },
+      { title: "A Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs"
+      , authors: "Paul He, Eddy Westbrook, Brent Carmer, Chris Phifer, Valentin Robert, Karl Smeltzer, Andrei Ştefănescu, Aaron Tomb, Adam Wick, Matthew Yacavone, Steve Zdancewic"
+      , conf: "OOPSLA 2021"
+      , url: "https://dl.acm.org/doi/10.1145/3485512"
+      , tags: ["coq", "plclub"]
+      },
+      { title: "Modular, Compositional, and Executable Formal Semantics for LLVM IR"
+      , authors: "Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva, Steve Zdancewic"
+      , conf: "ICFP 2021"
+      , url: "https://dl.acm.org/doi/10.1145/3473572"
+      , tags: ["coq", "monads", "plclub"]
+      },
+      { title: "Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL"
+      , authors: "Simon Foster, Chung-Kil Hur, Jim Woodlock"
+      , conf: "CONCUR 2021"
+      , url: "https://drops.dagstuhl.de/opus/volltexte/2021/14397/"
+      , tags: ["isabelle", "concurrency"]
+      }
+    ]
+  },
+  { year: 2022
+  , pubs: [
+      { title: "C4: Verified Transactional Objects"
+      , authors: "Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, Steve Zdancewic"
+      , conf: "OOPSLA 2022"
+      , url: "https://dl.acm.org/doi/10.1145/3527324"
+      , tags: ["coq", "concurrency", "plclub"]
+      },
+      { title: "Program Adverbs and Tlön Embeddings"
+      , authors: "Yao Li, Stephanie Weirich"
+      , conf: "ICFP 2022"
+      , url: "https://arxiv.org/abs/2207.05227"
+      , tags: ["coq", "plclub"]
+      },
+      { title: "Formal Reasoning About Layered Monadic Interpreters"
+      , authors: "Irene Yoon, Yannick Zakowski, Steve Zdancewic"
+      , conf: "ICFP 2022"
+      , url: "https://www.cis.upenn.edu/~euisuny/paper/fralmi.pdf"
+      , tags: ["coq", "monads", "plclub"]
+      },
+      { title: "Formally Verified Animation for RoboChart using Interaction Trees"
+      , authors: "Kangfeng Ye, Simon Foster, Jim Woodcock"
+      , conf: "ICFEM 2022"
+      , url: "https://eprints.whiterose.ac.uk/188566/"
+      , tags: ["isabelle", "concurrency"]
+      },
+      { title: "Conditional Contextual Refinement"
+      , authors: "Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur"
+      , conf: "Draft"
+      , url: "https://arxiv.org/abs/2203.07431"
+      , tags: ["coq", "concurrency"]
+      },
+      { title: "Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq"
+      , authors: "Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, Steve Zdancewic"
+      , conf: "Draft"
+      , url: "https://perso.ens-lyon.fr/yannick.zakowski/papers/ctrees_draft_non_anon.pdf"
+      , tags: ["coq", "concurrency", "plclub"]
+      }
+    ]
+  }
+] -%}

doc/runall

@@ -0,0 +1 @@
+jingoo -i index.html.jingoo -o index.html