## General Information

Like CS 4110 - Programming Languages and Logics, but on steroids. Much more mathematical in nature. This is intended as a “programming language theory crash course” for first-year PhD students at Cornell.

## Prerequisites

You probably want to know CS 3110 - Data Structures and Functional Programming and like CS 4110 - Programming Languages and Logics (for undergrads).

## Topics Covered

- Lambda calculus
- Inductive proof
- Operational semantics
- Language features and translation
- Continuation passing style
- Axiomatic semantics
- Denotational semantics
- Type systems and typed lambda calculus
- Linear logic, dependent types, and other advanced type systems

## Workload

(Spring 2011) Not too bad. Six homeworks, a prelim (with in-class and take-home portions), and a final. Homework can be done in groups.

(Spring 2017) Five homeworks, a take-home prelim, and a final. Homework can be done in pairs.

## General Advice

## Testimonials

I took CS 3110 - Data Structures and Functional Programming and CS 6110. I feel like this course was “too much information,” and I would have been happy with just CS 4110 - Programming Languages and Logics instead, since some of the proofs were tedious and some of the topics went a bit over my head.

This class was easy but boring.

(Spring 2017) This class was actually quite interesting and reasonably challenging, even for someone who had taken CS 4110 before. While they do overlap quite a bit in content, CS 6110 goes more into depth on advanced type theory (e.g. linear and dependent types), and I feel the proofs were presented better compared to CS 4110.

## Past Offerings

Semester | Time | Professor | Median Grade | Course Page |
---|---|---|---|---|

Spring 2011 | - | Nate Foster | - | http://www.cs.cornell.edu/Courses/cs6110/2011sp/syllabus.php |

Spring 2017 | MWF 10:10-11 AM | Adrian Sampson | - | https://www.cs.cornell.edu/courses/cs6110/2017sp/ |