From 697f08323724c0773c55954c372bdf1ec154f5b1 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 18 Aug 2024 15:05:55 -1000 Subject: [PATCH] Reference more future posts in SPA intro Signed-off-by: Danila Fedorin --- content/blog/00_spa_agda_intro.md | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/content/blog/00_spa_agda_intro.md b/content/blog/00_spa_agda_intro.md index 16fde26..1b9ff0e 100644 --- a/content/blog/00_spa_agda_intro.md +++ b/content/blog/00_spa_agda_intro.md @@ -88,7 +88,12 @@ I'd like to cover the following major topics, spending a couple of posts on each which is not at all compiler-centric. We need to connect these two, showing that the CFGs we produce "make sense" for our language, and that given CFGs that make sense, our analysis produces results that match the language's - execution. + execution. To do so, I write about the language and its semantics + in {{< draftlink "Part 5: Our Programming Language" "05_spa_agda_semantics" >}}, + then about building control flow graphs for the language in + {{< draftlink "Part 6: Control Flow Graphs" "06_spa_agda_cfg" >}}. + I then write about combining these two representations in + {{< draftlink "Part 7: Connecting Semantics and Control Flow Graphs" "07_spa_agda_semantics_and_cfg" >}}. ### Navigation @@ -98,3 +103,6 @@ Here are the posts that I’ve written so far for this series: * {{< draftlink "Combining Lattices" "02_spa_agda_combining_lattices" >}} * {{< draftlink "Lattices of Finite Height" "03_spa_agda_fixed_height" >}} * {{< draftlink "The Fixed-Point Algorithm" "04_spa_agda_fixedpoint" >}} +* {{< draftlink "Our Programming Language" "05_spa_agda_semantics" >}} +* {{< draftlink "Control Flow Graphs" "06_spa_agda_cfg" >}}. +* {{< draftlink "Connecting Semantics and Control Flow Graphs" "07_spa_agda_semantics_and_cfg" >}}.