Theory

We do not spend our time proving theorems on paper in our work in theoretical computer science. Instead, we use rich theorem proving environments and logical frameworks like PVS, MetaPRL, Coq, and Isabelle, combined with powerful automated first-order provers like Simplify, Sammy, haRVey, and CVCLite. Thus, our approach is typically much more detailed and rigorous as you cannot write a hand-wavey proof of correctness—you must prove every assertion in full detail.