Isabelle/HOL

Concrete Semantics - A Proof Assistant ApproachTobias Nipkow, Gerwin Klein

Isabelle/HOL - A Proof Assistant for Higher-Order LogicTobias Nipkow, Lawrence C. Paulson, Markus Wenzel