diff --git a/.gitignore b/.gitignore index 3f2de93a..c8e7f58e 100644 --- a/.gitignore +++ b/.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 diff --git a/DEV.md b/DEV.md index 94bef7d9..f5de9871 100644 --- a/DEV.md +++ b/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 diff --git a/doc/assets/github.svg b/doc/assets/github.svg new file mode 100644 index 00000000..e3da62ca --- /dev/null +++ b/doc/assets/github.svg @@ -0,0 +1 @@ + diff --git a/doc/assets/style.css b/doc/assets/style.css new file mode 100644 index 00000000..66970830 --- /dev/null +++ b/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; +} diff --git a/doc/index.html.jingoo b/doc/index.html.jingoo new file mode 100644 index 00000000..985b8328 --- /dev/null +++ b/doc/index.html.jingoo @@ -0,0 +1,55 @@ + + + + + + Interaction Trees + + + + + + +

Interaction Trees

+

Library

+
+

+Source Code +

+

Documentation

+ + + +
+

The Interaction Trees Academic Universe

+
+

List of publications about or closely related to Interaction Trees.

+ +{% for tag in ["coq", "isabelle", "vst", "monads", "coinduction", "testing", "concurrency", "plclub"] %} + + +{% endfor %} +{%- include "pubs.jingoo" -%} +{% for y in contents -%} +

{{ y.year }}

+ +{% endfor %} +
+ + diff --git a/doc/pubs.jingoo b/doc/pubs.jingoo new file mode 100644 index 00000000..fb8eef78 --- /dev/null +++ b/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"] + } + ] + } +] -%} diff --git a/doc/runall b/doc/runall new file mode 100644 index 00000000..4286d97b --- /dev/null +++ b/doc/runall @@ -0,0 +1 @@ +jingoo -i index.html.jingoo -o index.html