From 865d35f0a60bc7530bc906d8b096ab6f61aa2538 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Fri, 20 Sep 2024 16:22:48 +0100
Subject: [PATCH] [ bib ] adding plfa

---
 paper/paper.bib | 7 +++++++
 paper/paper.md  | 4 +++-
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/paper/paper.bib b/paper/paper.bib
index cc07d17ff9..95eb70c96b 100644
--- a/paper/paper.bib
+++ b/paper/paper.bib
@@ -1,3 +1,10 @@
+@Book{plfa22.08,
+    author = {Philip Wadler and Wen Kokke and Jeremy G. Siek},
+    title  = {Programming Language Foundations in {A}gda},
+    year   = {2022},
+    month  = aug,
+    url    = {https://plfa.inf.ed.ac.uk/22.08/},
+}
 @mastersthesis{ivardeBruin2023,
   author = {Ivar {de Bruin}},
   title = {Improving {Agda}'s module system},
diff --git a/paper/paper.md b/paper/paper.md
index 73c774c3ad..35c8ea4dbb 100644
--- a/paper/paper.md
+++ b/paper/paper.md
@@ -36,7 +36,7 @@ authors:
 	affiliation: 7
   - name: Hu, Jason Z. S.
 	orcid: 0000-0001-6710-6262
-	affiliation: 6 
+	affiliation: 6
   - name: Xia, Li-yiao
 	orcid: 0000-0003-2673-4400
 	affiliation: 8
@@ -111,6 +111,8 @@ Therefore, the standard library needs to provide all the necessary building bloc
 A wide range of projects, too numerous to list exhaustively, make use of `agda-stdlib`.
 A diverse selection of such projects, not intended as endorsements over any others, includes:
 
+- Programming Language Foundations in Agda [@plfa22.08]
+
 - Formalisation of category theory [@hu2021categories]
 
 - Intrinsically typed interpreters for imperative languages [@bach2017intrinsically] and formalisation of type-level computation and subtyping in Scala [@stucki2021theory].