Daniel's Blog

Welcome to my blog. Here, I write about various subjects, including (but not limited to) functional programming, compiler development, programming language theory, and occasionally video games. I hope you find something useful here!

• Implementing and Verifying "Static Program Analysis" in Agda, Part 5: Our Programming Language

  3794 words, about 18 minutes to read.

  In the previous several posts, I’ve formalized the notion of lattices, which are an essential ingredient to formalizing the analyses in Anders Møller’s lecture notes. ...

• Implementing and Verifying "Static Program Analysis" in Agda, Part 4: The Fixed-Point Algorithm

  2308 words, about 11 minutes to read.

  In the preivous post we looked at lattices of finite height, which are a crucial ingredient to our static analyses. In this post, I will describe the specific algorithm that makes use of these lattices; this algorithm will be at the core of this series. ...

• Implementing and Verifying "Static Program Analysis" in Agda, Part 3: Lattices of Finite Height

  7172 words, about 34 minutes to read.

  In the previous post, I introduced the class of finite-height lattices: lattices where chains made from elements and the less-than 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) “above-below” 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

  862 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. ...

• Microfeatures I Love in Blogs and Personal Websites

  3126 words, about 15 minutes to read.

  Some time ago, Hillel Wayne published an article titled Microfeatures I’d like to see in more languages . In this article, he described three kinds of features in programming languages: fundamental features, deeply engrained features, and nice-to-have convenience features. ...

• 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. ...

• Bergamot: Exploring Programming Language Inference Rules

  2421 words, about 12 minutes to read.

  Inference Rules and the Study of Programming Languages In this post, I will talk about inference rules, particularly in the field of programming language theory. ...