This is a follow-up on my previous post. It should be readable by itself if you just take a quick peek at herds.
Today, we are going to write type-checkers. And rewrite them. Again and again. Eventually, I’ll put in evidence that what seemed to be a programming hack in the last post turns out to be the difference between two well-known equivalent formulations of first-order logic, your good ol’ natural deduction and sequent calculus. Read the rest of this entry »