Daniel's Blog

Chapel's Runtime Types as an Interesting Alternative to Dependent Types

Implementing and Verifying "Static Program Analysis" in Agda, Part 9: Verifying the Forward Analysis

Implementing and Verifying "Static Program Analysis" in Agda, Part 8: Forward Analysis

Implementing and Verifying "Static Program Analysis" in Agda, Part 7: Connecting Semantics and Control Flow Graphs

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

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

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

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

Implementing and Verifying "Static Program Analysis" in Agda, Part 2: Combining Lattices

Untitled Short Story

Implementing and Verifying "Static Program Analysis" in Agda, Part 1: Lattices

Implementing and Verifying "Static Program Analysis" in Agda, Part 0: Intro

Microfeatures I Love in Blogs and Personal Websites

Integrating Agda's HTML Output with Hugo

The "Deeply Embedded Expression" Trick in Agda

Bergamot: Exploring Programming Language Inference Rules

My Favorite C++ Pattern: X Macros

The "Is Something" Pattern in Agda

Proving My Compiler Code Incorrect With Alloy

Search as a Polynomial

Generalizing Folds in Haskell

Declaratively Deploying Multiple Blog Versions with NixOS and Flakes

Digit Sum Patterns and Modular Arithmetic

Introducing Matrix Highlight

A Verified Evaluator for the Untyped Concatenative Calculus

Formalizing Dawn in Coq

Type-Safe Event Emitter in TypeScript

Approximating Custom Functions in Hugo

Pleasant Code Includes with Hugo

Advent of Code in Coq - Day 8

Advent of Code in Coq - Day 1

A Typesafe Representation of an Imperative Language

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

How Many Values Does a Boolean Have?

Meaningfully Typechecking a Language in Idris, With Tuples

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

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

Meaningfully Typechecking a Language in Idris, Revisited

Rendering Mathematics On The Back End

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

Building a Crystal Project with Nix, Revisited

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

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

Math Rendering is Wrong

Creating Recursive Functions in a Stack Based Language

Meaningfully Typechecking a Language in Idris

Building a Basic Crystal Project with Nix

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

Using GHC IDE for Haskell Error Checking and Autocompletion

A Language for an Assignment - Homework 3

A Language for an Assignment - Homework 2

A Language for an Assignment - Homework 1

JavaScript-Free Sidenotes in Hugo

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

Thoughts on Better Explanations

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

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

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

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

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

Switching to a Static Site Generator

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

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

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

Local Development Environment for JOS and CS 444

Lambda Calculus and Church Encoded Integers

Proof of Inductive Palindrome Definition in Coq

Setting Up Crystal on ARM

Haskell Error Checking and Autocompletion With LSP

A Look Into Starbound's File Formats

New Look, New Features!

Learning Emulation, Part 2.5 - Implementation

Learning Emulation, Part 2

Learning Emulation, Part 1

About

Content Graph

Favorites

Search