项目

A minimalist proof checker for intuitionistic propositional logic, implemented in Haskell. Verifies natural deduction proofs and normalizes them via the Curry–Howard correspondence.

An interactive visualization of complexity class relationships — P, NP, PSPACE, BPP, and more — with explanations of oracle separations and known inclusions.