Compare commits

..

4 Commits

Author SHA1 Message Date
8e4759bd2b Start on the navigation links in Agda SPA intro
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-30 20:52:33 -07:00
d2807917d2 Insert sequential links for series in analyze.rb
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-30 20:52:14 -07:00
71c030b947 Slightly tweak wording and front matter in Agda SPA posts
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-30 20:02:49 -07:00
1f3ab5349a Restore the dates in 'learning emulation' to their proper ones.
I found the original dates using the Wayback machine.

https://web.archive.org/web/20161022053013/https://danilafe.com/

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-30 18:58:38 -07:00
7 changed files with 33 additions and 13 deletions

View File

@ -35,6 +35,7 @@ end
data = {} data = {}
id = 0 id = 0
series = {}
files.each do |file| files.each do |file|
id += 1 id += 1
name = file name = file
@ -49,6 +50,12 @@ files.each do |file|
name = $~[1].delete_prefix('"').delete_suffix('"') name = $~[1].delete_prefix('"').delete_suffix('"')
elsif l =~ /^draft: true$/ elsif l =~ /^draft: true$/
draft = true draft = true
elsif l =~ /^series: (.+)$/
this_series = $~[1]
series_list = series.fetch(this_series) do
series[this_series] = []
end
series_list << file
elsif l =~ /^tags: (.+)$/ elsif l =~ /^tags: (.+)$/
tags = $~[1].delete_prefix("[").delete_suffix("]").split(/,\s?/).map { |it| it.gsub('"', '') } tags = $~[1].delete_prefix("[").delete_suffix("]").split(/,\s?/).map { |it| it.gsub('"', '') }
if tags.include? "Compilers" if tags.include? "Compilers"
@ -86,6 +93,14 @@ files.each do |file1|
edges << { :from => data[file1][:id], :to => data[ref][:id] } edges << { :from => data[file1][:id], :to => data[ref][:id] }
end end
end end
series.each do |series, files|
files.sort.each_cons(2) do |file1, file2|
next unless data[file1]
next unless data[file2]
edges << { :from => data[file1][:id], :to => data[file2][:id] }
edges << { :from => data[file2][:id], :to => data[file1][:id] }
end
end
edges.uniq edges.uniq
# edges.filter! { |e| e[:from] < e[:to] } # edges.filter! { |e| e[:from] < e[:to] }

View File

@ -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,
@ -85,6 +85,9 @@ for a post or two:
CFGs that make sense, our analysis produces results that match the language's CFGs that make sense, our analysis produces results that match the language's
execution. execution.
{{< todo >}}
Once the posts are ready, link them here to add some kind of navigation. ### Navigation
{{< /todo >}} Here are the posts that Ive written so far for this series:
* [Lattices]({{< relref "01_spa_agda_lattices" >}})
* [Combining Lattices]({{< relref "02_spa_agda_combining_lattices" >}})

View File

@ -1,6 +1,6 @@
--- ---
title: Learning Emulation, Part 1 title: Learning Emulation, Part 1
date: 2016-11-23 23:22:42.779811 date: 2016-06-27
tags: ["Emulation"] tags: ["Emulation"]
--- ---
I've decided that the purpose of a blog is to actually use it every once in a while. So, to fill up this blank space, I'll be documenting my own experience of starting to learn how emulation works. I'd like to say right now that my main goal was not to learn emulation. Rather, I needed to emulate to refresh my skills for a different subject area. However, emulation turned out fun enough to write about. I've decided that the purpose of a blog is to actually use it every once in a while. So, to fill up this blank space, I'll be documenting my own experience of starting to learn how emulation works. I'd like to say right now that my main goal was not to learn emulation. Rather, I needed to emulate to refresh my skills for a different subject area. However, emulation turned out fun enough to write about.

View File

@ -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"]
--- ---

View File

@ -1,6 +1,6 @@
--- ---
title: Learning Emulation, Part 2 title: Learning Emulation, Part 2
date: 2016-11-23 23:23:18.664038 date: 2016-06-29
tags: ["C", "Emulation"] tags: ["C", "Emulation"]
--- ---
_This is the second post in a series I'm writing about Chip-8 emulation. If you want to see the first one, head [here]({{< relref "/blog/01_learning_emulation.md" >}})._ _This is the second post in a series I'm writing about Chip-8 emulation. If you want to see the first one, head [here]({{< relref "/blog/01_learning_emulation.md" >}})._

View File

@ -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"]
--- ---

View File

@ -1,6 +1,6 @@
--- ---
title: Learning Emulation, Part 2.5 - Implementation title: Learning Emulation, Part 2.5 - Implementation
date: 2016-11-23 23:23:56.633942 date: 2016-06-30
tags: ["C", "Emulation"] tags: ["C", "Emulation"]
--- ---
_This is the third post in a series I'm writing about Chip-8 emulation. If you want to see the first one, head [here]({{< relref "/blog/01_learning_emulation.md" >}})._ _This is the third post in a series I'm writing about Chip-8 emulation. If you want to see the first one, head [here]({{< relref "/blog/01_learning_emulation.md" >}})._