Daniel's Blog

Posts

On this page you can see every article on this blog in reverse chronological order. If you like pretty colors and patterns, you can also see a visualization of all the articles and links between them on the content graph page. If you have something specific in mind, you can also try using the search page.

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

• Implementing and Verifying "Static Program Analysis" in Agda, Part 6: Control Flow Graphs

  3660 words, about 18 minutes to read.

  In the previous section, I’ve given a formal definition of the programming language that I’ve been trying to analyze. This formal definition serves as the “ground truth” for how our little imperative programs are executed; however, program analyses (especially in practice) seldom take the formal semantics as input. ...

• 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

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

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

• Declaratively Deploying Multiple Blog Versions with NixOS and Flakes

  3573 words, about 17 minutes to read.

  Prologue You can skip this section if you’d like. For the last few days, I’ve been stuck inside of my room due to some kind of cold or flu, which or may or may not be COVID™. ...

• Digit Sum Patterns and Modular Arithmetic

  6089 words, about 29 minutes to read.

  When I was in elementary school, our class was briefly visited by our school’s headmaster. He was there for a demonstration, probably intended to get us to practice our multiplication tables. ...

• Introducing Matrix Highlight

  1070 words, about 6 minutes to read.

  I wanted to briefly introduce a project that I’ve been working on in my spare time over the past couple of months. ...

• A Verified Evaluator for the Untyped Concatenative Calculus

  6826 words, about 33 minutes to read.

  Earlier, I wrote an article in which I used Coq to encode the formal semantics of Dawn’s Untyped Concatenative Calculus , and to prove a few things about the mini-language. ...

• Formalizing Dawn in Coq

  4373 words, about 21 minutes to read.

  The Foundations of Dawn article came up on Lobsters recently. In this article, the author of Dawn defines a core calculus for the language, and provides its semantics. ...

• Type-Safe Event Emitter in TypeScript

  1076 words, about 6 minutes to read.

  I’ve been playing around with TypeScript recently, and enjoying it too. Nearly all of my compile-time type safety desires have been accomodated by the language, and in a rather intuitive and clean way. ...

• Approximating Custom Functions in Hugo

  630 words, about 3 minutes to read.

  This will be an uncharacteristically short post. Recently, I wrote about my experience with including code from local files. After I wrote that post, I decided to expand upon my setup. ...

• Pleasant Code Includes with Hugo

  1826 words, about 9 minutes to read.

  Ever since I started the compiler series, I began to include more and more fragments of code into my blog. I didn’t want to be copy-pasting my code between my project and my Markdown files, so I quickly wrote up a Hugo shortcode to pull in other files in the local directory. ...

• Advent of Code in Coq - Day 8

  8609 words, about 41 minutes to read.

  Huh? We’re on day 8? What happened to days 2 through 7? Well, for the most part, I didn’t think they were that interesting from the Coq point of view. ...

• Advent of Code in Coq - Day 1

  3515 words, about 17 minutes to read.

  The first puzzle of this year’s Advent of Code was quite simple, which gave me a thought: “Hey, this feels within reach for me to formally verify! ...

• A Typesafe Representation of an Imperative Language

  4159 words, about 20 minutes to read.

  A recent homework assignment for my university’s programming languages course was to encode the abstract syntax for a small imperative language into Haskell data types. ...

• Compiling a Functional Language Using C++, Part 13 - Cleanup

  8297 words, about 39 minutes to read.

  In part 12, we added let/in and lambda expressions to our compiler. At the end of that post, I mentioned that before we move on to bigger and better things, I wanted to take a step back and clean up the compiler. ...

• How Many Values Does a Boolean Have?

  2084 words, about 10 minutes to read.

  A friend of mine recently had an interview for a software engineering position. They later recounted to me the content of the technical questions that they had been asked. ...

• Meaningfully Typechecking a Language in Idris, With Tuples

  2232 words, about 11 minutes to read.

  Some time ago, I wrote a post titled Meaningfully Typechecking a Language in Idris. I then followed it up with Meaningfully Typechecking a Language in Idris, Revisited. ...

• Time Traveling In Haskell: How It Works And How To Use It

  4296 words, about 21 minutes to read.

  I recently got to use a very curious Haskell technique in production: [note: As production as research code gets, anyway! ] time traveling. ...

• DELL Is A Horrible Company And You Should Avoid Them At All Costs

  3696 words, about 18 minutes to read.

  I really do not want this to be a consumer electronics blog. Such things aren’t interesting to me, and nor do I have much knowledge about them. ...

• Meaningfully Typechecking a Language in Idris, Revisited

  2970 words, about 14 minutes to read.

  Some time ago, I wrote a post titled Meaningfully Typechecking a Language in Idris. The gist of the post was as follows: ...

• Rendering Mathematics On The Back End

  2244 words, about 11 minutes to read.

  Due to something of a streak of bad luck when it came to computers, I spent a significant amount of time using a Linux-based Chromebook, and then a Pinebook Pro. ...

• Compiling a Functional Language Using C++, Part 12 - Let/In and Lambdas

  10322 words, about 49 minutes to read.

  Now that our language’s type system is more fleshed out and pleasant to use, it’s time to shift our focus to the ergonomics of the language itself. ...

• Building a Crystal Project with Nix, Revisited

  1191 words, about 6 minutes to read.

  As I’ve described in my previous post, the process for compiling a Crystal project with Nix is a fairly straightforward one. ...

• Compiling a Functional Language Using C++, Part 11 - Polymorphic Data Types

  4389 words, about 21 minutes to read.

  In part 10, we managed to get our compiler to accept functions that were polymorphically typed. However, a piece of the puzzle is still missing: while our functions can handle values of different types, the same cannot be said for our data types. ...

• Compiling a Functional Language Using C++, Part 10 - Polymorphism

  8124 words, about 39 minutes to read.

  In part 8, we wrote some pretty interesting programs in our little language. We successfully expressed arithmetic and recursion. But there’s one thing that we cannot express in our language without further changes: an if statement. ...

• Math Rendering is Wrong

  1543 words, about 8 minutes to read.

  Since I first started working on my website at age fourteen, the site has gone through many revisions, and hopefully changed for the better. ...

• Creating Recursive Functions in a Stack Based Language

  1996 words, about 10 minutes to read.

  In CS 381, Programming Language Fundamentals, many students chose to implement a stack based language. Such languages are very neat, but two of the requirements for such languages may, at first, seem somewhat hard to satisfy: ...

• Meaningfully Typechecking a Language in Idris

  2419 words, about 12 minutes to read.

  This term, I’m a TA for Oregon State University’s Programming Languages course. The students in the course are tasked with using Haskell to implement a programming language of their own design. ...

• Building a Basic Crystal Project with Nix

  769 words, about 4 minutes to read.

  I really like the idea of Nix: you can have reproducible builds, written more or less declaratively. I also really like the programming language Crystal , which is a compiled Ruby derivative. ...

• Compiling a Functional Language Using C++, Part 9 - Garbage Collection

  4832 words, about 23 minutes to read.

  “When will you learn? When will you learn that your actions have consequences?” So far, we’ve entirely ignored the problem of memory management. ...

• Using GHC IDE for Haskell Error Checking and Autocompletion

  629 words, about 3 minutes to read.

  Last year, when I took Oregon State University’s CS 381 class, I ended up setting up my editor with the Haskell IDE engine. ...

• A Language for an Assignment - Homework 3

  4155 words, about 20 minutes to read.

  It rained in Sunriver on New Year’s Eve, and it continued to rain for the next couple of days. So, instead of going skiing as planned, to the dismay of my family and friends, I spent the majority of those days working on the third language for homework 3. ...

• A Language for an Assignment - Homework 2

  1932 words, about 10 minutes to read.

  After the madness of the language for homework 1, the solution to the second homework offers a moment of respite. Let’s get right into the problems, shall we? ...

• A Language for an Assignment - Homework 1

  3918 words, about 19 minutes to read.

  On a rainy Oregon day, I was walking between classes with a group of friends. We were discussing the various ways to obfuscate solutions to the weekly homework assignments in our Algorithms course: replace every if with a ternary expression, use single variable names, put everything on one line. ...

• JavaScript-Free Sidenotes in Hugo

  1178 words, about 6 minutes to read.

  A friend recently showed me a website, the design of which I really liked: Gwern Branwen’s personal website . In particular, I found that sidenotes were a feature that I didn’t even know I needed. ...

• Compiling a Functional Language Using C++, Part 8 - LLVM

  4878 words, about 23 minutes to read.

  We don’t want a compiler that can only generate code for a single platform. Our language should work on macOS, Windows, and Linux, on x86_64, ARM, and maybe some other architectures. ...

• Thoughts on Better Explanations

  944 words, about 5 minutes to read.

  How do you explain how to write a program? Instructional material is becoming more and more popular on the web, with thousands of programming tutorials for languages, frameworks, and technologies created on YouTube, Medium, and peole’s personal sites. ...

• Compiling a Functional Language Using C++, Part 7 - Runtime

  2168 words, about 11 minutes to read.

  Wikipedia has the following definition for a runtime: A [runtime] primarily implements portions of an execution model. We know what our execution model is! ...

• Compiling a Functional Language Using C++, Part 6 - Compilation

  4976 words, about 24 minutes to read.

  In the previous post, we defined a machine for graph reduction, called a G-machine. However, this machine is still not particularly connected to our language. ...

• Compiling a Functional Language Using C++, Part 5 - Execution

  4439 words, about 21 minutes to read.

  We now have trees representing valid programs in our language, and it’s time to think about how to compile them into machine code, to be executed on hardware. ...

• Compiling a Functional Language Using C++, Part 4 - Small Improvements

  2150 words, about 11 minutes to read.

  We’ve done quite a big push in the previous post. We defined type rules for our language, implemented unification, and then implemented unification to enforce these rules for our program. ...

• Compiling a Functional Language Using C++, Part 3 - Type Checking

  5809 words, about 28 minutes to read.

  I think tokenizing and parsing are boring. The thing is, looking at syntax is a pretty shallow measure of how interesting a language is. ...

• Switching to a Static Site Generator

  575 words, about 3 minutes to read.

  A long time ago, I decided to try out Jekyll for my website. However, it all felt too convoluted: the ruby gems I needed to install, the configuration options for the site, the theming. ...

• Compiling a Functional Language Using C++, Part 2 - Parsing

  3679 words, about 18 minutes to read.

  In the previous post, we covered tokenizing. We learned how to convert an input string into logical segments, and even wrote up a tokenizer to do it according to the rules of our language. ...

• Compiling a Functional Language Using C++, Part 1 - Tokenizing

  1955 words, about 10 minutes to read.

  It makes sense to build a compiler bit by bit, following the stages we outlined in the first post of the series. ...

• Compiling a Functional Language Using C++, Part 0 - Intro

  975 words, about 5 minutes to read.

  During my last academic term, I was enrolled in a compilers course. We had a final project - develop a compiler for a basic Python subset, using LLVM. ...

• Local Development Environment for JOS and CS 444

  733 words, about 4 minutes to read.

  Working with the instructor’s dotfiles on the server is great and all, but there’s a few things you can do loccally that you can’t do on the school server: ...

• Lambda Calculus and Church Encoded Integers

  1847 words, about 9 minutes to read.

  You always hear the words “turning complete” thrown around in various contexts. Powerpoint is Turing complete, CSS is Turing complete. Turing completeness effectively describes a property of a language of system to perform any computation that can be performed on a computer (or by a human with a piece of paper). ...

• Proof of Inductive Palindrome Definition in Coq

  1408 words, about 7 minutes to read.

  Going through the Software Foundations textbook, I found an exercise which I really enjoyed solving. This exercise was to define an inductive property that holds iff a list is a palindrome. ...

• Setting Up Crystal on ARM

  792 words, about 4 minutes to read.

  Having found myself using a Chromebook with Arch Linux, I acutely felt the lack of official Crystal builds for ARM. After spending an hour or so looking online for a comprehensive guide to getting a working compiler on ARM, I think I now know the general idea. ...

• Haskell Error Checking and Autocompletion With LSP

  1551 words, about 8 minutes to read.

  For Oregon State University’s CS 381, Programming Language Fundamentals, Haskell is the language of choice. While it has an excellent REPL, and an excellent compiler, a piece of the puzzle is missing when writing Haskell code: on-the-fly error checking. ...

• A Look Into Starbound's File Formats

  2088 words, about 10 minutes to read.

  After playing a few hours of Starbound, I decided that I wanted to mess around with its file format, perhaps make a save manager/swapper, or something. ...

• New Look, New Features!

  107 words, about one minute to read.

  I’ve recently taken the time to redesign my website from scratch, on both the back-end and the front-end! On the back-end, this means the addition of tags, which allow me to categorize the not-so-plentiful content on the site. ...

• Learning Emulation, Part 2.5 - Implementation

  851 words, about 4 minutes to read.

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

• Learning Emulation, Part 2

  650 words, about 4 minutes to read.

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

• Learning Emulation, Part 1

  570 words, about 3 minutes to read.

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