Proof Pearl
An Intuitionistic Proof of a Discrete Form of the Jordan Curve Theorem Formalized in Coq with Combinatorial Hypermaps
On Process Equivalence = Equation Solving in CCS
Formalization and Implementation of Modern SAT Solvers