Tagged "Agda"

Implementing and Verifying "Static Program Analysis" in Agda, Part 3: Lattices of Finite Height
7168 words, about 34 minutes to read.
In the previous post, I introduced the class of finiteheight lattices: lattices where chains made from elements and the lessthan operator < can only be so long. ...

Implementing and Verifying "Static Program Analysis" in Agda, Part 2: Combining Lattices
5430 words, about 26 minutes to read.
In the previous post, I wrote about how lattices arise when tracking, comparing and combining static information about programs. I then showed two simple lattices: the natural numbers, and the (parameterized) “abovebelow” lattice, which modified an arbitrary set with “bottom” and “top” elements ($\bot$ and $\top$ respectively). ...

Implementing and Verifying "Static Program Analysis" in Agda, Part 1: Lattices
4965 words, about 24 minutes to read.
This is the first post in a series on static program analysis in Agda. See the introduction for a little bit more context. ...

Implementing and Verifying "Static Program Analysis" in Agda, Part 0: Intro
870 words, about 5 minutes to read.
Some years ago, when the Programming Languages research group at Oregon State University was discussing what to read, the Static Program Analysis lecture notes came up. ...

Integrating Agda's HTML Output with Hugo
4001 words, about 19 minutes to read.
One of my favorite things about Agda are its clickable HTML pages. If you don’t know what they are, that’s pages like Data. ...

The "Deeply Embedded Expression" Trick in Agda
2470 words, about 12 minutes to read.
I’ve been working on a relatively large Agda project for a few months now, and I’d like to think that I’ve become quite proficient. ...

The "Is Something" Pattern in Agda
1865 words, about 9 minutes to read.
Agda is a functional programming language with a relatively Haskelllike syntax and feature set, so coming into it, I relied on my past experiences with Haskell to get things done. ...