Slightly tweak wording and front matter in Agda SPA posts
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
1f3ab5349a
commit
71c030b947
|
@ -2,7 +2,7 @@
|
||||||
title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 0: Intro"
|
title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 0: Intro"
|
||||||
series: "Static Program Analysis in Agda"
|
series: "Static Program Analysis in Agda"
|
||||||
description: "In this post, I give a top-level overview of my work on formally verified static analyses"
|
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
|
draft: true
|
||||||
tags: ["Agda", "Programming Languages"]
|
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.
|
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
|
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,
|
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
|
I'd like to cover the following major topics, spending a couple of posts on each:
|
||||||
for a post or two:
|
|
||||||
|
|
||||||
* __Lattices__: the analyses I'm reasoning about use an algebraic structure
|
* __Lattices__: the analyses I'm reasoning about use an algebraic structure
|
||||||
called a _lattice_. This structure has certain properties that make it
|
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-based static program analysis, the various elements of the
|
||||||
lattice represent different facts or properties that we know about the
|
lattice represent different facts or properties that we know about the
|
||||||
program in question; operations on the lattice help us combine these facts
|
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
|
Interestingly, lattices can be made by combining other lattices in certain
|
||||||
ways. We can therefore use simpler lattices as building blocks to create
|
ways. We can therefore use simpler lattices as building blocks to create
|
||||||
more complex ones, all while preserving the algebraic structure that
|
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
|
* __The Fixed-Point Algorithm__: to analyze a program, we use information
|
||||||
that we already know to compute additional information. For instance,
|
that we already know to compute additional information. For instance,
|
||||||
|
|
|
@ -1,7 +1,8 @@
|
||||||
---
|
---
|
||||||
title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 1: Lattices"
|
title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 1: Lattices"
|
||||||
series: "Static Program Analysis in Agda"
|
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
|
draft: true
|
||||||
tags: ["Agda", "Programming Languages"]
|
tags: ["Agda", "Programming Languages"]
|
||||||
---
|
---
|
||||||
|
|
|
@ -1,7 +1,8 @@
|
||||||
---
|
---
|
||||||
title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 2: Combining Lattices"
|
title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 2: Combining Lattices"
|
||||||
series: "Static Program Analysis in Agda"
|
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
|
draft: true
|
||||||
tags: ["Agda", "Programming Languages"]
|
tags: ["Agda", "Programming Languages"]
|
||||||
---
|
---
|
||||||
|
|
Loading…
Reference in New Issue
Block a user