15-816 Linear Logic | Spring 2012 | | Frank Pfenning | | MW 12:00-1:20 | | GHC 4303 | | 12 units | This graduate course provides an introduction to linear logic with an emphasis on its applications in computer science. This includes the theory of functional, logic, imperative, and concurrent programming languages. We will also develop a linear type theory which will serve as a meta-language in which the theory of programming languages with state can be formalized effectively. Prerequisites: This is an introductory graduate course with no formal prerequisites, but an exposure to functional programming and type systems would be helpful. Enterprising undergraduates are welcome to attend this course. Remote participation: Lectures will be video-recorded and possibly simulcast. If you are interested in taking this course remotely, please contact the instructor.
What's New? - (Fri 5/11) The final has been graded. Here are links to the final exam and a sample solution.
- (Mon 5/7) Notes for Lecture 22 have been posted. This completes the set of lectures for which we intend to post notes.
- (Sun 5/6) Notes for Lecture 25 have been posted.
- (Sun 5/6) Lectures notes for Lectures 20, 21, 23, 24, and 28 have been posted to the schedule page.
- (Mon 4/23) Lecture 18 on Resource Management have been posted.
- (Thu 4/19) Assignment 7 has been posted. Problems from Assignment 5 and Assignment 6 are also still eligible. Due on Wed May 2.
- (Fri 4/14) Celf code for Lecture 22 on Concurrent Monadic Computations.
- (Fri 4/13) Notes for Lecture 17 on Backward Chaining have been posted.
- (Thu 4/12) Updated instructions for downloading and installing the most recent version of Celf. You can, for example, now specify multiple files to load on the command line.
- (Thu 4/12) Assignment 6 has been posted. Problems from Assignment 5 are also still eligible. Due on Wed Apr 18.
- (Mon 4/2) Notes for Lecture 16 on Ordered Forward Chaining have been posted.
- (Wed 3/28) Assignment 5 has been posted, the LaTeX support updated.
- Prior versions of this course:
Class Material Course Information | Lectures | Mon Wed 12:00-1:30, GHC 4303 | | Live Video | IP 128.2.186.93
Tandberg codec C90 | | Office Hours | Thu 12:00-1:00, Google Hangout
Thu 1:00-2:00, GHC 9101 | | Mailing List | linlog-course@cs.cmu.edu (subscribe) | | Notes | There is no textbook, but lecture notes and papers will be handed out. | | Credit | 12 units | | Grading | 60% Homework, 15% Midterm, 25% Final | | Homework | Weekly homework is assigned each Monday and due the following Monday.
Late homework will be accepted only under exceptional circumstances. | | Midterm | Wed Mar 7, in class.
Closed book. | | Final | Tue May 8, 8:30-11:30am, GHC 4215
Closed book. | | Topics | Intuitionistic and classical linear logic
Natural deduction and sequent calculi
Focused proofs
Describing state-based systems
Session types for concurrent processes
Linear logic programming
Linear type theory and logical frameworks
Imperative programming languages
Linear type systems and functional languages
Structural complexity via linearity
Linearity and concurrency
Other substructural logics | | Home | http://www.cs.cmu.edu/~fp/courses/15816-s12/ |
[ Home | Schedule | Assignments | Handouts | Software | Resources ] fp@cs
Frank Pfenning |