codex-semantics-library · mlemerre · May 21, 2025 · Apr 18, 2025 · Apr 24, 2025 · Apr 24, 2025
diff --git a/Gemfile b/Gemfile
@@ -7,4 +7,5 @@ gem "github-pages"
 gem "webrick"
 gem "jekyll-redirect-from"
 gem "jekyll-email-protect"
-
+gem "kramdown-math-katex"
+gem "therubyracer" # JS engine to run katex
diff --git a/Gemfile.lock b/Gemfile.lock
@@ -13,6 +13,7 @@ GEM
       minitest (>= 5.1)
       securerandom (>= 0.3)
       tzinfo (~> 2.0, >= 2.0.5)
+      uri (>= 0.13.1)
     addressable (2.8.7)
       public_suffix (>= 2.0.2, < 7.0)
     base64 (0.2.0)
@@ -43,7 +44,16 @@ GEM
       logger
     faraday-net_http (3.4.0)
       net-http (>= 0.5.0)
+    ffi (1.17.0-aarch64-linux-gnu)
+    ffi (1.17.0-aarch64-linux-musl)
+    ffi (1.17.0-arm-linux-gnu)
+    ffi (1.17.0-arm-linux-musl)
+    ffi (1.17.0-arm64-darwin)
+    ffi (1.17.0-x86-linux-gnu)
+    ffi (1.17.0-x86-linux-musl)
+    ffi (1.17.0-x86_64-darwin)
     ffi (1.17.0-x86_64-linux-gnu)
+    ffi (1.17.0-x86_64-linux-musl)
     forwardable-extended (2.6.0)
     gemoji (4.1.0)
     github-pages (232)
@@ -221,10 +231,21 @@ GEM
       jekyll-include-cache
       jekyll-seo-tag (>= 2.0)
       rake (>= 12.3.1)
+    katex (0.10.0)
+      execjs (~> 2.8)
     kramdown (2.4.0)
       rexml
+    kramdown-math-katex (1.0.1)
+      katex (~> 0.4)
+      kramdown (~> 2.0)
     kramdown-parser-gfm (1.1.0)
       kramdown (~> 2.0)
+    libv8 (3.16.14.19.1)
+    libv8 (3.16.14.19.1-arm-linux)
+    libv8 (3.16.14.19.1-universal-darwin)
+    libv8 (3.16.14.19.1-x86-linux)
+    libv8 (3.16.14.19.1-x86_64-darwin)
+    libv8 (3.16.14.19.1-x86_64-linux)
     liquid (4.0.4)
     listen (3.9.0)
       rb-fsevent (~> 0.10, >= 0.10.3)
@@ -238,6 +259,16 @@ GEM
     minitest (5.25.1)
     net-http (0.5.0)
       uri
+    nokogiri (1.16.7-aarch64-linux)
+      racc (~> 1.4)
+    nokogiri (1.16.7-arm-linux)
+      racc (~> 1.4)
+    nokogiri (1.16.7-arm64-darwin)
+      racc (~> 1.4)
+    nokogiri (1.16.7-x86-linux)
+      racc (~> 1.4)
+    nokogiri (1.16.7-x86_64-darwin)
+      racc (~> 1.4)
     nokogiri (1.16.7-x86_64-linux)
       racc (~> 1.4)
     octokit (4.25.1)
@@ -251,6 +282,7 @@ GEM
     rb-fsevent (0.11.2)
     rb-inotify (0.11.1)
       ffi (~> 1.0)
+    ref (2.0.0)
     rexml (3.3.9)
     rouge (3.30.0)
     rubyzip (2.3.2)
@@ -267,6 +299,9 @@ GEM
     simpleidn (0.2.3)
     terminal-table (1.8.0)
       unicode-display_width (~> 1.1, >= 1.1.1)
+    therubyracer (0.12.3)
+      libv8 (~> 3.16.14.15)
+      ref
     typhoeus (1.4.1)
       ethon (>= 0.9.0)
     tzinfo (2.0.6)
@@ -276,14 +311,28 @@ GEM
     webrick (1.9.0)
 
 PLATFORMS
+  aarch64-linux
+  aarch64-linux-gnu
+  aarch64-linux-musl
+  arm-linux
+  arm-linux-gnu
+  arm-linux-musl
+  arm64-darwin
+  x86-linux
+  x86-linux-gnu
+  x86-linux-musl
+  x86_64-darwin
   x86_64-linux
+  x86_64-linux-musl
 
 DEPENDENCIES
   github-pages
   jekyll-email-protect
   jekyll-redirect-from
   just-the-docs (= 0.10.0)
+  kramdown-math-katex
+  therubyracer
   webrick
 
 BUNDLED WITH
-   2.3.26
+   2.5.23
diff --git a/_config.yml b/_config.yml
@@ -38,4 +38,8 @@ exclude: [
 
 plugins:
   - jekyll-redirect-from
-  - jekyll-email-protect  
+  - jekyll-email-protect
+
+markdown: kramdown
+kramdown:
+  math_engine: katex
diff --git a/_data/publications.yml b/_data/publications.yml
@@ -4,6 +4,25 @@
 #
 # Make sure all paths start with "/", espacially the easy-summary one,
 # otherwise the _layout/paper.html WILL break (it looks into this DB for a matching entry)
+- year: 2025
+  publications:
+    - title: Relational Abstractions Based on Labeled Union-Find
+      authors:
+        - name: Dorian Lesbre
+        - name: Matthieu Lemerre
+        - name: Hichem Rami Ait-El-Hara
+        - name: François Bobot
+      venue: 46th ACM-SIGPLAN Symposium on Programming Language Design and Implementation
+      venue-acronym: PLDI
+      doi: 10.1145/3729298
+      artifact: https://zenodo.org/records/15165896
+      bibtex: /assets/publications/bibtex/2025-pldi-relational-abstractions-labeled-uf.bib
+      easy-summary: /papers/2025-pldi-relational-abstractions-labeled-uf.html
+      pdf-with-appendix: /assets/publications/pdfs/2025-pldi-relational-abstractions-labeled-uf-with-appendices.pdf
+      topics:
+        - relational abstract domain
+        - labeled union-find
+        - abstract interpretation
 - year: 2024
   publications:
     - title: "A Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level Code"
@@ -15,12 +34,12 @@
       venue-acronym: OOPSLA
       artifact: https://zenodo.org/records/13383433
       artifact-evaluated-reusable: true
-      artifact-available: true      
+      artifact-available: true
       easy-summary: /papers/2024-oopsla-typedc-dependent-nominal-physical-type-system.html
       pdf: /assets/publications/pdfs/2024-oopsla-full-with-appendices.pdf
       talk-slides: /assets/publications/slides/2024-oopsla-typedc-dependent-nominal-physical-typesystem.pdf
       bibtex: /assets/publications/bibtex/2024-oopsla-typedc-dependent-nominal-typesystem.bib
-#      talk-video: TODO
+      #      talk-video: TODO
       topics:
         - abstract interpretation
         - memory safety
@@ -39,9 +58,9 @@
       artifact-custom-image-height: "70"
       easy-summary: /papers/2024-sas-trace-partitioning-as-an-optimization-problem.html
       pdf: /assets/publications/pdfs/2024-sas-tpop.pdf
-#      bibtex: TODO
-#      talk-slides: TODO
-#      talk-video: TODO
+      #      bibtex: TODO
+      #      talk-slides: TODO
+      #      talk-video: TODO
       topics:
         - abstract interpretation
         - trace partitioning

diff --git a/_includes/head_custom.html b/_includes/head_custom.html
@@ -21,3 +21,7 @@
 {% for css in page.css %}
 <link rel="stylesheet" href="/assets/css/{{ css }}.css">
 {% endfor %}
+{% if page.katex %}
+<link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.12.0/dist/katex.min.css" integrity="sha384-AfEj0r4/OFrOo5t7NnNe46zW/tFgW6x/bCJG8FqQCEo3+Aro6EYUG4+cU+KJWu/X" crossorigin="anonymous">
+<style>.katex { font-size: 1rem; }</style>
+{% endif %}
diff --git a/assets/publications/bibtex/2024-pldi-compiling-with-abstract-interpretation.bib b/assets/publications/bibtex/2024-pldi-compiling-with-abstract-interpretation.bib
@@ -1,3 +1,4 @@
+% The main publication - which is most likely the one you'll want to cite
 @article{10.1145/3656392,
   author = {Lesbre, Dorian and Lemerre, Matthieu},
   title = {Compiling with Abstract Interpretation},
@@ -16,13 +17,15 @@ @article{10.1145/3656392
   keywords = {Compilers, Abstract Interpretation, Static Single Assignment, SSA},
 }
 
+% The extended version - includes appendices and proofs
 @techreport{hal-04535159,
   author = {Lesbre, Dorian and Lemerre, Matthieu},
   title = {Compiling with Abstract Interpretation (with appendices)},
   year = {2024},
   url = {https://hal.science/hal-04535159},
 }
 
+% The associated software artifact
 @misc{10.5281/zenodo.10895582,
   author = {Dorian Lesbre and Matthieu Lemerre},
   title = {Compiling with Abstract Interpretation: Artifact},

diff --git a/assets/publications/bibtex/2025-pldi-relational-abstractions-labeled-uf.bib b/assets/publications/bibtex/2025-pldi-relational-abstractions-labeled-uf.bib
@@ -0,0 +1,41 @@
+% The main publication - which is most likely the one you'll want to cite
+@article{10.1145/3729298,
+  author = {Lesbre, Dorian and Lemerre, Matthieu and Ait-El-Hara, Hichem Rami
+            and Bobot, François},
+  title = {Relational Abstractions Based on Labeled Union-Find},
+  month = 6,
+  year = 2025,
+  journal = {Proc. {ACM} Program. Lang.},
+  issn = {2475-1421},
+  number = {{PLDI}},
+  volume = {9},
+  articleno = {195},
+  publisher = {Association for Computing Machinery},
+  address = {New York, NY, USA},
+  doi = {10.1145/3729298},
+}
+
+% The extended version - includes appendices and proofs
+@techreport{hal-05029216,
+  author = {Lesbre, Dorian and Lemerre, Matthieu and Ait-El-Hara, Hichem Rami
+            and Bobot, François},
+  title = {Relational Abstractions Based on Labeled Union-Find (with appendices)
+           },
+  month = apr,
+  year = 2025,
+  publisher = {HAL},
+  url = {https://hal.science/hal-05029216},
+}
+
+% The associated software artifact
+@software{10.5281/zenodo.15165896,
+  author = {Lesbre, Dorian and Lemerre, Matthieu and Ait-El-Hara, Hichem Rami
+            and Bobot, François},
+  title = {Artifact for paper "Relational Abstractions Based on Labeled
+           Union-Find" },
+  month = apr,
+  year = 2025,
+  publisher = {Zenodo},
+  doi = {10.5281/zenodo.15165896},
+  url = {https://doi.org/10.5281/zenodo.15165896},
+}