Substructural Logics
Course ID 15836
Description This graduate course provides an introduction to substructural logics, such as linear, ordered, affine, bunched, or separation logic, with an emphasis on their applications in computer science. This includes the design and theory of programming constructs for concurrent message-passing computation and techniques for specifying and reasoning about programming languages in the form of substructural operational semantics.
Key Topics
Deduction inference, substructural natural deduction, sequent calculus, cut elimination, computation as proof reduction, combining logics, polarization and focusing, computation as proof construction, substructural logical frameworks, Lambek calculus, substructural type systems in programming languages.
Required Background Knowledge
This is an introductory graduate course with no formal prerequisites, but an exposure to functional programming and type systems may be helpful.
Course Relevance
Advanced undergraduates, master's, and doctoral students in CSD, Philosophy, Math, and ECE are welcome
Course Goals
After taking this course students will be able to: - model stateful, concurrent, and resource-aware systems in substructural logics - define and reason about programming languages using substructural operational semantics - capture computational phenomena in advanced substructural type theories - apply the judgmental method to define logics and type theories for a rich variety of applications - appreciate the deep philosophical underpinnings and elegance of the computation-as-proof-reduction and computation-as-proof-construction paradigms
Learning Resources
Lecture notes and course software will be distributed
Assessment Structure
Grades will be based on a homework assignments, midterm exam, miniproject, and possibly final exam (score distribution is TBA)
Extra Time Commitment
n/a
Course Link
https://www.cs.cmu.edu/~fp/courses/15836-f23/