
Questions Schedule 
 DESCRIPTION:

This course provides a thorough introduction to modern constructive logic, its roots in philosophy, its numerous applications in computer science, and its mathematical properties. The core topics of this course are intuitionistic logic, natural deduction, CurryHoward isomorphism, propositions as types, proofs as programs, formulas as programs, functional programming, logic programming, Heyting arithmetic and primitive recursion, cut elimination, connections between classical and constructive logic, inductive definitions, sequent calculus, and decidable classes. Advanced topics may include type theory, proof search, linear logic, temporal logic, modal logic.
Students who successfully complete this course will:
 Understand the working principles of logic
 Understand how the meaning of a proposition comes from its verifications
 Distinguish propositions from judgments
 Use proof rules to conduct formal proofs
 Formalize informal problems into precise logical language
 Justify how proof rules fit to one another in sound and complete ways
 Assess the validity of a formal proof
 Understand propositions as types, proofs as programs, formulas as programs
 Relate constructive logic to computation and constructive proofs to functional programs
 Relate deductive proof search to computation in logic programming
 Relate induction to recursion and use induction to prove properties in and about logical systems
 Understand the principles and applications of logic programming
 MORE INFORMATION:
 See prior instances of similar courses at Carnegie Mellon University in Fall 2015 and Fall 2016 and Spring 2020 and Spring 2021 by André Platzer and earlier by Frank Pfenning, Karl Crary for more information on prior versions of this course.