From 71c030b947b97fd6d9f6ea311c76866c5ad758eb Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 30 May 2024 20:02:49 -0700 Subject: [PATCH] Slightly tweak wording and front matter in Agda SPA posts Signed-off-by: Danila Fedorin --- content/blog/00_spa_agda_intro.md | 10 +++++----- content/blog/01_spa_agda_lattices.md | 3 ++- content/blog/02_spa_agda_combining_lattices.md | 3 ++- 3 files changed, 9 insertions(+), 7 deletions(-) diff --git a/content/blog/00_spa_agda_intro.md b/content/blog/00_spa_agda_intro.md index 2539ecd..90802f7 100644 --- a/content/blog/00_spa_agda_intro.md +++ b/content/blog/00_spa_agda_intro.md @@ -2,7 +2,7 @@ title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 0: Intro" series: "Static Program Analysis in Agda" description: "In this post, I give a top-level overview of my work on formally verified static analyses" -date: 2024-04-12T14:23:03-07:00 +date: 2024-05-30T19:36:58-07:00 draft: true tags: ["Agda", "Programming Languages"] --- @@ -37,8 +37,7 @@ this milestone, I'd like to pause and talk about what I've done. In subsequent posts in this series, will describe what I have so far. It's not perfect, and some work is yet to be done; however, getting to this point was no joke, and I think it's worth discussing. In all, -I envision three major topics to cover, each of which is likely going to make -for a post or two: +I'd like to cover the following major topics, spending a couple of posts on each: * __Lattices__: the analyses I'm reasoning about use an algebraic structure called a _lattice_. This structure has certain properties that make it @@ -46,12 +45,13 @@ for a post or two: lattice-based static program analysis, the various elements of the lattice represent different facts or properties that we know about the program in question; operations on the lattice help us combine these facts - and reason about them. + and reason about them. I write about this in [Part 1: Lattices]({{< relref "01_spa_agda_lattices" >}}). Interestingly, lattices can be made by combining other lattices in certain ways. We can therefore use simpler lattices as building blocks to create more complex ones, all while preserving the algebraic structure that - we need for program analysis. + we need for program analysis. I write about this in + [Part 2: Combining Lattices]({{< relref "02_spa_agda_combining_lattices" >}}). * __The Fixed-Point Algorithm__: to analyze a program, we use information that we already know to compute additional information. For instance, diff --git a/content/blog/01_spa_agda_lattices.md b/content/blog/01_spa_agda_lattices.md index 89dff36..55cdf12 100644 --- a/content/blog/01_spa_agda_lattices.md +++ b/content/blog/01_spa_agda_lattices.md @@ -1,7 +1,8 @@ --- title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 1: Lattices" series: "Static Program Analysis in Agda" -date: 2024-04-13T14:23:03-07:00 +description: "In this post, I introduce an algebraic structure called a lattice, which underpins certain program analyses" +date: 2024-05-30T19:36:59-07:00 draft: true tags: ["Agda", "Programming Languages"] --- diff --git a/content/blog/02_spa_agda_combining_lattices.md b/content/blog/02_spa_agda_combining_lattices.md index a6d9bad..6b131ee 100644 --- a/content/blog/02_spa_agda_combining_lattices.md +++ b/content/blog/02_spa_agda_combining_lattices.md @@ -1,7 +1,8 @@ --- title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 2: Combining Lattices" series: "Static Program Analysis in Agda" -date: 2024-04-13T14:23:03-07:01 +description: "In this post, I describe how lattices can be combined to create other, more complex lattices" +date: 2024-05-30T19:37:00-07:00 draft: true tags: ["Agda", "Programming Languages"] ---