Add functional essence PLDI paper that uses Iris.

logsem · Jul 15, 2024 · b8d1587 · b8d1587
1 parent a95b316
commit b8d1587
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 0 deletions.
diff --git a/_data/publications.json b/_data/publications.json
@@ -8,6 +8,17 @@
       "where_published": "To appear in Journal of the ACM (JACM), 2024",
       "pdf_url": "pdfs/2024-jacm-logical-type-soundness.pdf"
     },
+      {
+        "title": "The Functional Essence of Imperative Binary Search Trees",
+        "authors": [
+	    "Anton Lorenzen",
+	    "Daan Leijen",
+	    "Wouter Swierstra",
+	    "Sam Lindley"
+        ],
+        "where_published": "In PLDI 2024: ACM SIGPLAN International Conference on Programming Language Design and Implementation",
+        "pdf_url": "pdfs/2024-pldi-functional-essence.pdf",
+      },
       {
         "title": "Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq",
         "authors": [

diff --git a/pdfs/2024-pldi-functional-essence.pdf b/pdfs/2024-pldi-functional-essence.pdf