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 7: Connecting Semantics and Control Flow Graphs

  4192 words, about 20 minutes to read.

  In the previous two posts, I covered two ways of looking at programs in my little toy language: In part 5, I covered the formal semantics of the programming language. ...

  Latest in series: Implementing and Verifying "Static Program Analysis" in Agda

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

• My Favorite C++ Pattern: X Macros

  4185 words, about 20 minutes to read.

  When I first joined the Chapel team, one pattern used in its C++-based compiler made a strong impression on me. Since then, I’ve used the pattern many more times, and have been very satisfied with how it turned out. ...

• The "Is Something" Pattern in Agda

  1865 words, about 9 minutes to read.

  Agda is a functional programming language with a relatively Haskell-like syntax and feature set, so coming into it, I relied on my past experiences with Haskell to get things done. ...

• Proving My Compiler Code Incorrect With Alloy

  6969 words, about 33 minutes to read.

  Disclaimer: though “my compiler code” makes for a fun title, I do not claim exclusive credit for any of the C++ code in the Chapel compiler that I mention in this post. ...

• Search as a Polynomial

  3733 words, about 18 minutes to read.

  I read a really neat paper some time ago, and I’ve been wanting to write about it ever since. The paper is called Algebras for Weighted Search , and it is a tad too deep to dive into in a blog article – readers of ICFP are rarely the target audience on this site. ...

• Generalizing Folds in Haskell

  3372 words, about 16 minutes to read.

  Have you encountered Haskell’s foldr function? Did you know that you can use it to express any function on a list? ...