290C - Logic, Computation, and Programming Languages

This course will examine the close connection between formal logic, computation, and programming languages. The two primary areas of investigation will be (1) various systems of formal logic and their connection to different type systems via the Curry-Howard Correspondence; and (2) various fragments of first-order logic and their connection to logic programming languages. The class will involve both understanding the theory behind these connections and implementing these ideas in practice. A basic knowledge of first-order logic is assumed, but a deep background in logic is not required. The exact topics studied will be largely driven by student interest.