Computer Assisted Reasoning
Formalizing an Analytic Proof of the Prime Number Theorem
Mechanized Semantics for the Clight Subset of the C Language
Social Choice Theory in HOL
Rewriting Conversions Implemented with Continuations