
 DESCRIPTION:
 Dynamic logics are multimodal logics whose modalities of necessity and possibility state logical properties of all or some executions of a given program in a programming language. They can be used as specification and verification logics for programs. Since dynamic logics are proper logics closed under all operators, they can be used to state many different types of questions about the behavior of programs. Since dynamic logics have a compositional semantics, their reasoning principles can be captured in axioms and proof rules for compositional verification of programs. Dynamic logics also enable the study of meta theory such as soundness, (relative) completeness, and expressiveness. Overall, dynamic logics excel at providing simple and elegant logical foundations for reasoning about programs or dynamical systems. This course will study the proof theory and meta theory of dynamic logics, including foundations for proof procedures.

Students who successfully complete this course will be able to:
 Identify how programming languages principles manifest in dynamic logic.
 Capture the semantics of programming languages via their Kripke semantics.
 Use dynamic logic reasoning to rigorously specify and verify properties of programs.
 Recognize correct and incorrect reasoning principles for programs.
 Appreciate theoretical foundations of program analysis
Topics tentatively include the following:
 Firstorder logic
 Modal logic
 Dynamic logic
 Regular programs
 Kripke semantics
 Correspondence theory
 Hilbert calculi
 Sequent calculi
 Tableaux calculi
 Interpreted versus uninterpreted logic
 Soundness and completeness
 Expressiveness
 Canonical models and filtration
 Infinitary and finitary axiomatizations
 Herbrand's theorem
 Kleene algebra
 Axiom Schemata vs. Axioms
 PREREQUISITES:
 This is a graduate course with no formal prerequisites, but prior exposure to logic or programming language principles may be helpful.
 METHOD OF EVALUATION:
 Grading will be based on a midterm exam as well as a selfdefined final course project. Exams are closed book with one doublesided sheet of handwritten notes permitted.