Abstract interpretation using laziness:
proving Conway's Lost

Cosmological Theorem

Abstract:

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.

Host: Frank Pfenning

Appointments: Jennifer Landefeld <jennsbl@cs.cmu.edu>

Friday, December 8, 2006

3:30 p.m.

Wean Hall 8220

Principles
of Programming Seminars