From 51dd82f4142dde31fe3e799f4ec013724a0013ad Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Fri, 29 Jul 2022 00:19:55 +0100 Subject: [PATCH 1/8] jingoo --- .gitignore | 4 +- doc/HOME.md | 10 +++++ doc/pubs.jingoo | 104 ++++++++++++++++++++++++++++++++++++++++++++++++ doc/runall | 1 + 4 files changed, 118 insertions(+), 1 deletion(-) create mode 100644 doc/HOME.md create mode 100644 doc/pubs.jingoo create mode 100644 doc/runall 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/doc/HOME.md b/doc/HOME.md new file mode 100644 index 00000000..efc0f039 --- /dev/null +++ b/doc/HOME.md @@ -0,0 +1,10 @@ +Interaction Trees +================= + +## Source Code + +https://github.com/DeepSpec/InteractionTrees + +## The Interaction Trees Academic Universe + +List of publications about or closely related to Interaction Trees. diff --git a/doc/pubs.jingoo b/doc/pubs.jingoo new file mode 100644 index 00000000..caeafa92 --- /dev/null +++ b/doc/pubs.jingoo @@ -0,0 +1,104 @@ +{%- for y in [ + { 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" + } + ] + }, + { 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" + }, + { 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" + }, + { 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" + } + ] + }, + { 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" + }, + { 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" + }, + { 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/" + }, + { 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" + }, + { 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" + }, + { 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/" + } + ] + }, + { 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" + }, + { title: "Program Adverbs and Tlön Embeddings" + , authors: "Yao Li, Stephanie Weirich" + , conf: "ICFP 2022" + , url: "https://arxiv.org/abs/2207.05227" + }, + { 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" + }, + { 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/" + }, + { title: "Conditional Contextual Refinement" + , authors: "Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur" + , conf: "Draft" + , url: "https://arxiv.org/abs/2203.07431" + }, + { 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" + } + ] + } +] -%} +## {{ y.year }} + +{% for pub in y.pubs -%} +{{ pub.title }} +{% endfor %} +{% endfor %} diff --git a/doc/runall b/doc/runall new file mode 100644 index 00000000..b4c8a335 --- /dev/null +++ b/doc/runall @@ -0,0 +1 @@ +jingoo -i pubs.jingoo -o index.html From b4bd06f1136b1c63831f7bc3b5ed44abeca55232 Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Fri, 29 Jul 2022 09:14:14 +0100 Subject: [PATCH 2/8] DEV.md: Use gh-pages instead of doc --- DEV.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) 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 From 9953be1e756f5f924c520094e79846a70ce5da92 Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Fri, 29 Jul 2022 10:22:15 +0100 Subject: [PATCH 3/8] Basic style --- doc/HOME.md | 10 ---------- doc/assets/github.svg | 1 + doc/assets/style.css | 25 +++++++++++++++++++++++++ doc/index.html.jingoo | 43 +++++++++++++++++++++++++++++++++++++++++++ doc/pubs.jingoo | 10 ++-------- doc/runall | 2 +- 6 files changed, 72 insertions(+), 19 deletions(-) delete mode 100644 doc/HOME.md create mode 100644 doc/assets/github.svg create mode 100644 doc/assets/style.css create mode 100644 doc/index.html.jingoo diff --git a/doc/HOME.md b/doc/HOME.md deleted file mode 100644 index efc0f039..00000000 --- a/doc/HOME.md +++ /dev/null @@ -1,10 +0,0 @@ -Interaction Trees -================= - -## Source Code - -https://github.com/DeepSpec/InteractionTrees - -## The Interaction Trees Academic Universe - -List of publications about or closely related to Interaction Trees. 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..adf83ea6 --- /dev/null +++ b/doc/assets/style.css @@ -0,0 +1,25 @@ +.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-authors { + color: gray; +} + +.pub-paper::after { + content: '🖹'; + vertical-align: middle; + margin-left: 0.3em; + font-size: 1.2em; +} + +.level-2 { + margin-left: 2em; +} diff --git a/doc/index.html.jingoo b/doc/index.html.jingoo new file mode 100644 index 00000000..f839fe75 --- /dev/null +++ b/doc/index.html.jingoo @@ -0,0 +1,43 @@ + + + + + + Interaction Trees + + + + + + +

Interaction Trees

+

Library

+
+

+Source Code +

+

Documentation

+ +
+

The Interaction Trees Academic Universe

+
+

List of publications about or closely related to Interaction Trees.

+{%- include "pubs.jingoo" -%} +{% for y in contents -%} +

{{ y.year }}

+
    +{% for pub in y.pubs -%} +
  • +
    {{ pub.title }}
    +
    by {{ pub.authors }}
    +
    {{ pub.conf }}. Paper
    +
    • +{% endfor %} +
+{% endfor %} +
+ + diff --git a/doc/pubs.jingoo b/doc/pubs.jingoo index caeafa92..4e6cdcd8 100644 --- a/doc/pubs.jingoo +++ b/doc/pubs.jingoo @@ -1,4 +1,4 @@ -{%- for y in [ +{%- set contents = [ { year: 2019 , pubs: [ { title: "From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server" @@ -40,7 +40,7 @@ , url: "https://dl.acm.org/doi/abs/10.1145/3460319.3464798" }, { 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" + , 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/" }, @@ -96,9 +96,3 @@ ] } ] -%} -## {{ y.year }} - -{% for pub in y.pubs -%} -{{ pub.title }} -{% endfor %} -{% endfor %} diff --git a/doc/runall b/doc/runall index b4c8a335..4286d97b 100644 --- a/doc/runall +++ b/doc/runall @@ -1 +1 @@ -jingoo -i pubs.jingoo -o index.html +jingoo -i index.html.jingoo -o index.html From d901f6138d73e363910e0ec143813733fc72266b Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Fri, 29 Jul 2022 10:49:54 +0100 Subject: [PATCH 4/8] More style --- doc/assets/style.css | 9 +++++++-- doc/index.html.jingoo | 6 +++--- 2 files changed, 10 insertions(+), 5 deletions(-) diff --git a/doc/assets/style.css b/doc/assets/style.css index adf83ea6..dc1579f2 100644 --- a/doc/assets/style.css +++ b/doc/assets/style.css @@ -9,8 +9,9 @@ width: 1.3em; } -.pub-authors { - color: gray; +.pub-title > a { + text-decoration: none; + font-weight: bold; } .pub-paper::after { @@ -23,3 +24,7 @@ .level-2 { margin-left: 2em; } + +li { + margin-bottom: 0.7em; +} diff --git a/doc/index.html.jingoo b/doc/index.html.jingoo index f839fe75..664d38d2 100644 --- a/doc/index.html.jingoo +++ b/doc/index.html.jingoo @@ -31,9 +31,9 @@
    {% for pub in y.pubs -%}
  • -
    {{ pub.title }}
    -
    by {{ pub.authors }}
    -
    {{ pub.conf }}. Paper
    +
    {{ pub.title }}
    +
    by {{ pub.authors }}
    +
    {{ pub.conf }}
    • {% endfor %}
From c6bb04163ccabb74e13f3764047d015e6395b85e Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Fri, 29 Jul 2022 18:02:37 +0100 Subject: [PATCH 5/8] Update style --- doc/assets/style.css | 11 +++++++++-- doc/index.html.jingoo | 6 ++++-- 2 files changed, 13 insertions(+), 4 deletions(-) diff --git a/doc/assets/style.css b/doc/assets/style.css index dc1579f2..cd0a2345 100644 --- a/doc/assets/style.css +++ b/doc/assets/style.css @@ -1,3 +1,7 @@ +h1, h2 { + text-align: center; +} + .github::after { display: inline-flex; content: ''; @@ -15,10 +19,8 @@ } .pub-paper::after { - content: '🖹'; vertical-align: middle; margin-left: 0.3em; - font-size: 1.2em; } .level-2 { @@ -28,3 +30,8 @@ li { margin-bottom: 0.7em; } + +.item-paper::marker { + content: '🖹 '; + font-size: 1.2em; +} diff --git a/doc/index.html.jingoo b/doc/index.html.jingoo index 664d38d2..f812ad36 100644 --- a/doc/index.html.jingoo +++ b/doc/index.html.jingoo @@ -19,8 +19,10 @@

Documentation

+ +

The Interaction Trees Academic Universe

@@ -30,7 +32,7 @@

{{ y.year }}

    {% for pub in y.pubs -%} -
  • +
  • {{ pub.title }}
    by {{ pub.authors }}
    {{ pub.conf }}
    From 37eebdc66dc96d37886a923ce2f33c7760b4ac53 Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Fri, 29 Jul 2022 19:42:50 +0100 Subject: [PATCH 6/8] Fancy filters --- doc/assets/style.css | 63 ++++++++++++++++++++++++++++++++++++++++++- doc/index.html.jingoo | 14 ++++++++-- doc/pubs.jingoo | 16 +++++++++++ 3 files changed, 90 insertions(+), 3 deletions(-) diff --git a/doc/assets/style.css b/doc/assets/style.css index cd0a2345..185f39c9 100644 --- a/doc/assets/style.css +++ b/doc/assets/style.css @@ -28,10 +28,71 @@ h1, h2 { } li { - margin-bottom: 0.7em; + 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; } + +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 index f812ad36..985b8328 100644 --- a/doc/index.html.jingoo +++ b/doc/index.html.jingoo @@ -27,15 +27,25 @@

    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 }}

      {% for pub in y.pubs -%} -
    • +
    • {{ pub.title }}
      by {{ pub.authors }}
      -
      {{ pub.conf }}
      +
      + {{ pub.conf }} + {%- for tag in pub.tags %} + {{ tag }} + {%- endfor -%} +
      • {% endfor %}
    diff --git a/doc/pubs.jingoo b/doc/pubs.jingoo index 4e6cdcd8..fb8eef78 100644 --- a/doc/pubs.jingoo +++ b/doc/pubs.jingoo @@ -5,6 +5,7 @@ , 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"] } ] }, @@ -14,16 +15,19 @@ , 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"] } ] }, @@ -33,31 +37,37 @@ , 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"] } ] }, @@ -67,31 +77,37 @@ , 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"] } ] } From cfa75a3bca2d3266f476babe32ff7f137cdf6588 Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Fri, 29 Jul 2022 19:59:37 +0100 Subject: [PATCH 7/8] Fix margins --- doc/assets/style.css | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/doc/assets/style.css b/doc/assets/style.css index 185f39c9..b844ea9d 100644 --- a/doc/assets/style.css +++ b/doc/assets/style.css @@ -23,8 +23,8 @@ h1, h2 { margin-left: 0.3em; } -.level-2 { - margin-left: 2em; +@media only screen and (min-width: 768px) { + .level-2 { margin-left: 2em; } } li { @@ -72,6 +72,7 @@ input + label { .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; } From 83159a84146daf3a8712570094c1a99aac17b571 Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Wed, 3 Aug 2022 20:34:05 +0100 Subject: [PATCH 8/8] doc: Set fonts --- doc/assets/style.css | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/doc/assets/style.css b/doc/assets/style.css index b844ea9d..66970830 100644 --- a/doc/assets/style.css +++ b/doc/assets/style.css @@ -1,4 +1,11 @@ +@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; }