About

I’m an engineer and researcher interested in a variety of subjects related to math, computer science, economics, etc.

Intent

My intent is for this blog to be a compendium of:

Writings about books, papers or small side projects that I undertake for the purpose of learning, in the hope that my distillations will be useful to others (generally marked “Exposition”).
Widgets that I build in the course of those investigations (code will generally be shared, but use it at your own risk).
Writing about any novel insights or ideas that I may have related to my interests (generally marked “Research”).

Subject Areas

I’ll try to keep everything roughly organized by subject, ideally in some sort of pedagogical ordering. Right now, there’s only one subject:

Reasoning
- E-Graphs
  - E-Graph Basics
- Proofs

Errors

Please let me know if you see any errors.

Recent Posts

Typing Rules

How can we tell if a term is well-typed? How can we tell if an environment is well-formed? We can be sure we have formed a proper term and environment (in the Calculus of…

Conversion Rules

Now that we can represent some basic theorems using a computer, we need to be able manipulate those representations. We also will want to be able to tell if two types are…

Calculus of Constructions

To verify (or prove) theorems using a computer, we need some way to represent a theorem and the steps used to prove it. The Calculus of Constructions (CoC) forms the basis…

E-Graph Basics

An e-graph (equivalence graph) is a type of data structure commonly used to reason about equalities and programs computationally.