Posts about: Programming

Brief writeup on how to utilize the Curry-Howard correspondence to check natural deduction proofs encoded in Haskell at compile-time. ( ´ ▽ ` )ﾉ

Sequent is a Fitch-style first-order logic proof language and web app for checking, formatting, and rendering proofs with clickable diagnostics.