The aim of this course will be to provide introduction to some applications of logic in computer science. Following are some possible topics. At least three of these will be covered in some detail. Actual choice of topics, including depth and breadth, will depend on interest/background of the class.
Communication and Concurrency: Processes as transition systems, operations on these processes (composition, hiding etc.). Bisimulation and observational equivalences. Calculus of mobile systems: pi-calculus. Some theory related to pi calculus. Logics to reason about transition systems, LTL, CTL* and modal mu calculus.
Reasoning about Knowledge: Knowledge as modality, axioms of knowledge. Common knowledge, distributed agents exchanging messages, agreeing to disagree. Logical omniscience.
Finite Model Theory: Expressiveness of FO and its extensions on finite structures. Games for lower bounds. Connections with complexity classes, role of order on the domain.
Feasible Proofs: Propositional proof systems for tautologies. Simulation and lower bounds on length of proofs for specific systems (e.g. PHP requires superpolynomial length using resolution). Theories of weak arithmetic, provably total functions and relations to complexity theory.
Full Abstraction problem for PCF: PCF as an extension of lambda calculus. Operational and denotational semantics and the full abstraction problem. Solutions to the full abstraction problem. Games semantics.
R. Milner, Communicating and Mobile Systems: the pi calculus, Cambridge University press, 1999.
R. Fagin, J. Y. Halpern, Y. Moses, M. Y. Vardi, Reasoning about Knowledge, MIT press, 1995.
H. D. Ebbinghaus, J. Flum, Finite Model Theory, Springer, 1995 (2nd edition has also appeared a couple of years back).
N. Immerman, Descriptive Complexity, Springer, 1999.
J. Krajicek, Bounded Arithmetic, Propositional Logic and Complexity Theory, Cambridge university press, 1995.
Research papers (to be recommended during the course).