POP Seminar, 02-07-03

I describe an abstract interpretation technique based on lazy functional programming, and apply it to the proof of Conway's Lost Cosmological Theorem, a combinatorial proposition analogous to the four color theorem or Kepler's conjecture. By the semantics of Haskell, evaluating a predicate on a partial lazy list to True proves that the predicate would evaluate to True on any list extending the partial list. In this way proving a property of all lists can be reduced to evaluating the property on sufficiently many partial lists, which cover the set of all lists. The proof is completed by proving the correctness of the code implementing the predicate by hand. The oracle that chooses a covering set of partial lists need not be verified. In this way the amount of program code which must be verified by hand in order to complete the proof is greatly reduced, increasing confidence in the result.