A research blog about programming languages, formal logics, software development and their interactions, by Matthias Puech.

Tag: herd

Reverse natural deduction and get sequent calculus

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 »

Reversing data structures

A reversed list is not really a list anymore. It is isomorphic to a list, but it is not a list. Let me explain why. Read the rest of this entry »