• A self-verifying theorem prover 

    Davis, Jared Curran (2009-12)
    Programs have precise semantics, so we can use mathematical proof to establish their properties. These proofs are often too large to validate with the usual "social process" of mathematics, so instead we create and check ...