Proof Theory

Catalog description

This course teaches the theory of proofs studied as a formal and mathematical object. The language of proofs emerged as a natural place where programming languages, category theory, and complexity meet, and is becoming increasingly popular in the study of type systems, denotational semantics, concurrency theory, implicit complexity, and higher-order model checking to name a few. Tools include mathematical abstraction, theorem provers, the representation of proofs in multiple formalisms (sequent calculus, natural deduction, proof nets and their semantics) and multiple systems, as well as studying their relative expressivity and complexity. The goals are to excel in formal reasoning, have a precise and actionable understanding of the expressivity of a system compared to others, improve mathematical reasoning and the capacity to navigate between multiple representations of the same proof. Lecture Hours: 3 Repeatability: May not be repeated for credit. Grade Mode: Normal, Audit Schedule Type (Primary): Lecture Click here for the Schedule of Classes.