Constructive Logic Course ID 15657 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 counts as a Fundamentals course in the Computer Science major. Key Topics Modern constructive logic and its roots in philosophy, intuitionistic logic; Inductive definitions; Functional programming; Type theory; Logic programming; Proof search; Logical frameworks Required Background Knowledge Basis in functional programming Course Relevance Those interested in learning about some the many applications of logical reasoning in computer science. 15-657 is for graduate students. Undergraduates should enroll in 15-317. 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 Learning Resources Piazza; Lecture Notes Assessment Structure Assignments: 40%; Midterms: 30%; Final: 30% Course Link https://lfcps.org/course/constlog.html
