Add distinguished paper

Author: yannl35133

pandoc/paper.lua

@@ -4,6 +4,7 @@ function jsondata(data)
 
   newdata.title = data.title or {}
   newdata.url = data.url or ""
+  newdata.award = data.award
   newdata.authors = data.authors or {}
   newdata.venue = data.venue
   newdata.year = data.year
@@ -19,6 +20,9 @@ function yamldata(data)
 
   newdata.title = pandoc.utils.stringify(data["title"])
   newdata.url = pandoc.write(pandoc.Pandoc{data["url"]}, 'html')
+  if data.award then
+    newdata.award = pandoc.utils.stringify(data["award"])
+  end
   newdata.authors = data["authors"] or {}
   if data.venue then
     newdata.venue = pandoc.utils.stringify(data["venue"])
@@ -46,6 +50,7 @@ function paper(data)
 
   local title = data.title
   local url = data.url
+  local award = data.award
   local authors = data.authors
   local venue = data.venue
   local year = data.year
@@ -59,6 +64,17 @@ function paper(data)
     header = { title }
   end
 
+  if award then
+    local icon = "<i class=\"fa-solid fa-award\"></i>"
+    local html_output = string.format(
+      "<span>%s %s</span>",
+      icon, award
+    )
+    award = pandoc.RawBlock("html", html_output)
+  else
+    award = {}
+  end
+
   local sub = {}
 
   if venue and year then
@@ -110,6 +126,7 @@ function paper(data)
 
   local div_content = {
     pandoc.Header(3, header),
+    pandoc.Div(award, {class= "award"}),
     pandoc.Div(authors, {class = "authors"}),
     pandoc.Para(sub),
     pandoc.Div(file_info, {class = "files"})

src/index.md

@@ -14,7 +14,7 @@ side-by-side: true
 orcid: 0009-0005-6461-2801
 # dblp: https://dblp.org/pid/384/4150.html
 # scholar: https://scholar.google.com/
-# hal: https://hal.science/
+hal: https://hal.science/search/index/q/*/authIdHal_s/yann-leray
 # mastodon: 
 github: Yann-Leray
 # gitlab: 
@@ -30,7 +30,8 @@ footer: >-
 I am a PhD student in [Gallinette](https://gallinette.gitlabpages.inria.fr/website/) under the supervision of [Nicolas Tabareau](https://tabareau.fr), [Matthieu Sozeau](https://mattam.org) and [Théo Winterhalter](https://theowinterhalter.github.io).
 
 I am mostly interested in formally proving proof assistants correct, including all necessary properties of their underlying type theory.
-I also wrote the implementation of [rewrite rules in Coq](https://coq.inria.fr/refman/addendum/rewrite-rules.html), with help from [Théo](https://theowinterhalter.github.io), Gaëtan Gilbert and the rest of the Coq development team.
+I also wrote the implementation of [rewrite rules in Rocq](https://rocq-prover.org/refman/addendum/rewrite-rules.html), with help from [Théo](https://theowinterhalter.github.io), Gaëtan Gilbert and the rest of the Rocq development team.
+I am now maintainer for Rocq's kernel, especially on matters relating to its guard condition and guard checker.
 
 
 # Publications
@@ -39,15 +40,19 @@ I also wrote the implementation of [rewrite rules in Coq](https://coq.inria.fr/r
 
 ``` yaml {.papers}
 papers:
-  - title: "The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant"
-    authors: Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter
-    venue: International Conference on Interactive Theorem Proving (ITP 2024)
+  - title: "Encode the Cake and Eat It Too: Controlling Computation in Type Theory, Locally"
+    award: "Distinguished Paper"
+    authors: Yann Leray, Théo Winterhalter
+    venue: Proceedings of the ACM on Programming Languages (POPL 2026)
     # year: 2024
-    doi: https://doi.org/10.4230/LIPIcs.ITP.2024.26
+    doi: https://doi.org/10.1145/3776704
     files:
       - text: Paper
         type: pdf
-        src: https://doi.org/10.4230/LIPIcs.ITP.2024.26
+        src: https://doi.org/10.1145/3776704
+      - text: Artifact
+        type: code
+        src: https://doi.org/10.5281/zenodo.17524818
   - title: "Observational Equality Meets CIC"
     authors: Loïc Pujet, Yann Leray, Nicolas Tabareau
     venue: ACM Transactions on Programming Languages and Systems (TOPLAS 2025)
@@ -57,23 +62,21 @@ papers:
       - text: Paper
         type: pdf
         src: https://doi.org/10.1145/3719342
+  - title: "The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant"
+    authors: Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter
+    venue: International Conference on Interactive Theorem Proving (ITP 2024)
+    # year: 2024
+    doi: https://doi.org/10.4230/LIPIcs.ITP.2024.26
+    files:
+      - text: Paper
+        type: pdf
+        src: https://doi.org/10.4230/LIPIcs.ITP.2024.26
 ```
 
 ## Talks
 
 ``` yaml {.papers}
 papers:
-  - title: "The Rewster: The Coq Proof Assistant with Rewrite Rules"
-    authors: Gaëtan Gilbert, Yann Leray, Nicolas Tabareau, Théo Winterhalter
-    venue: 29th International Conference on Types for Proofs and Programs (TYPES 2023)
-    # year: 2023
-    files:
-      - text: Slides
-        type: pdf
-        src: https://types2023.webs.upv.es/slides/S18/TYPES2023-Gilbert-Leray-Tabareau-Winterhalter.pdf
-      - text: Recording
-        type: video
-        src: https://media.upv.es/#/portal/video/bf2591f0-34a6-11ee-8485-f133f82f8945
   - title: "How (not) to prove typed type conversion transitive"
     authors: Yann Leray
     venue: 31st International Conference on Types for Proofs and Programs (TYPES 2025)
@@ -85,6 +88,17 @@ papers:
       - text: Recording
         type: video
         src: https://youtu.be/edwdMMpRKoc
+  - title: "The Rewster: The Coq Proof Assistant with Rewrite Rules"
+    authors: Gaëtan Gilbert, Yann Leray, Nicolas Tabareau, Théo Winterhalter
+    venue: 29th International Conference on Types for Proofs and Programs (TYPES 2023)
+    # year: 2023
+    files:
+      - text: Slides
+        type: pdf
+        src: https://types2023.webs.upv.es/slides/S18/TYPES2023-Gilbert-Leray-Tabareau-Winterhalter.pdf
+      - text: Recording
+        type: video
+        src: https://media.upv.es/#/portal/video/bf2591f0-34a6-11ee-8485-f133f82f8945
 ```
 <!-- 
 # Education

website/style.css

@@ -335,6 +335,24 @@ div.files a:hover {
   text-decoration: none;
 }
 
+div.award {
+  display: flex;
+  justify-content: flex-start;
+  flex-direction: row;
+  flex-wrap: wrap;
+  align-items: baseline;
+  gap: 5px 0;
+}
+
+div.award span {
+  border-radius: 5px;
+  padding: 4px 6px 0px 4px;
+  margin-bottom: 4px;
+  margin-right: 5px;
+  background: #d0f6d5;
+  color: #00b34a;
+}
+
 span.lastupdate {
   color: #9e9d9d;
 }