Formal models of computation such as finite state automata, pushdown automata and Turing machines. Formal definitions of languages, problems, and language classes including recursive, recursively enumerable, regular, and context free languages. The relationships among various models of computation, language classes, and problems. Church's thesis and the limits of computability. Proofs of program properties including correctness.