In this four-lecture course we will survey some fundamental connections between logic and theoretical computer science. From the beginning, computer science was strongly influenced by results and methods from logic. Vice versa, the computer as a universal tool gave directions for the development of modern logic.
In the first lecture we will discuss theoretical and practical limitations of computers: undecidability and incompleteness of logics, turing machines, NP, PSPACE and other complexity classes. The second lecture deals with constructivism and the synthesis of algorithms from proofs, intuitionistic logic, lambda calculus and logic programming. Topic of the third lecture is the use of logic for the specification of computing systems: we will compare the model-theoretic expressiveness of finite automata and various logics. Finally, the fourth lecture is an introduction to program verification, automated theorem proving and model checking.
The lectures are largely independent and require no special knowledge. There will be a set of exercises in each lecture for those students willing to take the course for credit.