From e91b6f692fc460100e2fd3af1a92ce655799a55c Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 6 Jul 2024 17:39:03 -0700 Subject: [PATCH] Publish introducton to SPA in Agda Signed-off-by: Danila Fedorin --- content/blog/00_spa_agda_intro.md | 24 ++++++++++++------- .../static-program-analysis-in-agda/_index.md | 1 - themes/vanilla | 2 +- 3 files changed, 16 insertions(+), 11 deletions(-) diff --git a/content/blog/00_spa_agda_intro.md b/content/blog/00_spa_agda_intro.md index 8707c37..088a487 100644 --- a/content/blog/00_spa_agda_intro.md +++ b/content/blog/00_spa_agda_intro.md @@ -2,8 +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-05-30T19:36:58-07:00 -draft: true +date: 2024-07-06T17:37:42-07:00 tags: ["Agda", "Programming Languages"] --- @@ -45,13 +44,13 @@ I'd like to cover the following major topics, spending a couple of posts on each 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. I write about this in [Part 1: Lattices]({{< relref "01_spa_agda_lattices" >}}). + and reason about them. I write about this in {{< draftlink "Part 1: Lattices" "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. I write about this in - [Part 2: Combining Lattices]({{< relref "02_spa_agda_combining_lattices" >}}). + {{< draftlink "Part 2: Combining Lattices" "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, @@ -65,9 +64,15 @@ I'd like to cover the following major topics, spending a couple of posts on each What does it mean for the output to stop changing? Roughly, that's when the following equation holds: `knownInfo = analyze(knownInfo)`. In mathematics, this is known as a [fixed point](https://mathworld.wolfram.com/FixedPoint.html). - Crucially, not all functions have fixed points; however, certain types of - functions on lattices do. The fixed-point algorithm is a way to compute these - points, and we will use this to drive our analyses. + To enable computing fixed points, we focus on a specific kind of lattices: + those with a _fixed height_. I talk about what this means in + {{< draftlink "Part 3: Lattices of Finite Height" "03_spa_agda_fixed_height" >}}. + + Even if we restrict our attention to lattices of fixed height, + not all functions have fixed points; however, certain types of functions on + lattices always do. The _fixed-point algorithm_ is a way to compute these + points, and we will use this to drive our analyses. I talk + about this in {{< draftlink "Part 4: The Fixed-Point Algorithm" "04_spa_agda_fixedpoint" >}}. * __Correctness__: putting together the work on lattices and the fixed-point algorithm, we can implement a static program analyzer in Agda. However, @@ -89,5 +94,6 @@ I'd like to cover the following major topics, spending a couple of posts on each ### Navigation Here are the posts that I’ve written so far for this series: -* [Lattices]({{< relref "01_spa_agda_lattices" >}}) -* [Combining Lattices]({{< relref "02_spa_agda_combining_lattices" >}}) +* {{< draftlink "Lattices" "01_spa_agda_lattices" >}} +* {{< draftlink "Combining Lattices" "02_spa_agda_combining_lattices" >}} +* {{< draftlink "Lattices of Finite Height" "03_spa_agda_fixed_height" >}} diff --git a/content/series/static-program-analysis-in-agda/_index.md b/content/series/static-program-analysis-in-agda/_index.md index e5fe242..32bceff 100644 --- a/content/series/static-program-analysis-in-agda/_index.md +++ b/content/series/static-program-analysis-in-agda/_index.md @@ -7,6 +7,5 @@ summary = """ analyzer for a simple language. """ status = "ongoing" -draft = true divider = ": " +++ diff --git a/themes/vanilla b/themes/vanilla index f931e6e..c00867d 160000 --- a/themes/vanilla +++ b/themes/vanilla @@ -1 +1 @@ -Subproject commit f931e6eceb79affac3563bba398ebe9bbbbe26a3 +Subproject commit c00867d46bf88c6ee31b52894120d7579f4c3070