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
|