Posts

A Proof of the Schröder-Bernstein Theorem in ACL2

Monad is a Monad is a Monad

The Curry-Howard Correspondence

A Fistful of Axioms

A Few of my Favorite Tactics

Coq Equality IV

Coq Equality III

Coq Equality II

Coq Equality I