|
- DESCRIPTION:
- Dynamic logics are multi-modal 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:
- First-order 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 self-defined final course project. Exams are closed book with one double-sided sheet of hand-written notes permitted.