Constructive Logic

Course ID 15317

Description This multidisciplinary junior-level course is designed to provide a thorough introduction to modern constructive logic, its roots in philosophy, its numerous applications in computer science, and its mathematical properties. Some of the topics to be covered are intuitionistic logic, inductive definitions, functional programming, type theory, realizability, connections between classical and constructive logic, decidable classes. This course 15-317 is for undergraduates. Graduate students should enroll in 15-657.

Key Topics
Modern constructive logic and its roots in philosophy, intuitionistic logic; Inductive definitions; Functional programming; Type theory; Logic programming; Proof search; Logical frameworks

Learning Resources
Piazza; Lecture Notes

Course Relevance
Those interested in learning about some the many applications of logical reasoning in computer science.

Course Goals
Understand how logics: are defined; what they mean; how they are used in computer science
Develop skills in all types of logic: classical, constructive, intuitionistic

Pre-required Knowledge
Basis in functional programming

Assessment Structure
Assignments: 40%; Midterms: 30%; Final: 30%

Extra Time Commitments
15-317 is for undergraduates. Graduate students should register for 15-357.

Course Link
https://lfcps.org/course/constlog.html