Intrinsic theories: a methodology for reasoning about functional programs and their computational complexity

We present a general methodology for reasoning about functional programs, which uses as axioms only the properties most intrinsic to the data type in hand, and treats programs as auxiliary axioms. Its advantages include expressive flexibility, minimal axiomatics, dispensing with coding for reasoning about partial functions, data genericity, and a clear conceptual framework for machine-independent characterizations of a wide spectrum of computational complexity classes.

LS Home page or Talks in 1998/99