CS 456: Programming Languages

LWSN 1106 10:30a-11:20a MWF

about

Instructor:

Ben Delaware

bendy at purdue.edu

Office Hours: Mondays 2:00-3:30p in LWSN 2116M

Teaching Assistant:

Robert Dickerson

dicker18 at purdue.edu

Office Hours: TBD

Course Description:

This is a course on the principles of programming languages and their application. The emphasis is on ideas and techniques relevant to practitioners, but includes theoretical foundations crucial for deeper understanding: abstract syntax, formal semantics, type systems, and abstraction. Work in the course involves exploring programming languages and features as both a user (by writing programs in those languages) and a language designer (by implementing interpreters for various languages), and as a scholar (by proving mathematical properties of them). We will investigate language-based techniques for analyzing program behavior, and discuss what guarantees a programming language can provide its users about the abstractions it provides. The course will also offer some historical perspective on the evolution of programming languages and why some designs thrive while others fail. Upon successfully completing this course, students will be able to:

  1. Write programs in two languages with state-of-the-art type systems, Rust and Haskell.
  2. Compare and contrast different language-provided abstractions, including ad-hoc and parametric polymorphism, user-defined data types, and static and dynamic memory safety.
  3. Precisely formulate the syntax and runtime behavior of a programming language.
  4. Specify different notions of safety for a programming language and employ language-based techniques to ensure the safety of programs.

The first half of the course will discuss these topics in the context of the (mostly) pure functional language, Haskell, while the second half will use the modern systems language Rust.

logistics

A Proviso:

Brightspace is the definitive repository for up-to-date information about the course; this webpage provides a publicly accessible overview of CS 456.

Lectures:

Lectures will be Mondays, Wednesdays, and Fridays in LWSN 1106, which students are expected to attend. If you are sick or otherwise unable to attend a lecture, please let the instructor know as soon as possible. All lecture materials, including slides and related readings, will be made available on brightpsace after class.

Office Hours:

Each Monday, the instructor will have office hours from 2:00-3:30p in LWSN 2116M, and the TA will hold regular office hours somewhere (TBD). In the event that students cannot attend scheduled office hours, they should contact the instructor via email to schedule a time to meet individually.

Homeworks:

Homeworks will be posted (roughly) every other week according to the course schedule. Homeworks are to be submitted via Brightspace by 6PM on their assigned due date. Make sure that any programs compile without errors (and ideally without any warnings). If they do not, they will not be graded. Everyone will receive three courtesy late days for the semester. Once all these days have been used, students will need to notify the instructor or the TA ahead of time with an explanation and plan for completion. These requests will be accepted at my discretion and may include a point penalty of 5% per day late. Asking for an extension does not guarantee it will be granted.

Course Project:

This course project asks students to either implement a suggested project in either Rust or Haskell, or to propose and implement a project of their choosing. Projects can be completed either individually or in groups of two. As these projects are less structured than the homeworks, there will be three milestones to help keep you on track. A list of project ideas and a timeline will be posted on Brightspace.

success

How to Succeed in this Course

In order to be successful, students should be familiar with:

  1. Programming in an imperative language, e.g. Java / C / Python, etc.
  2. Basic logic and proofs techniques found in an undergraduate discrete math course like CS182: sets, relations, functions, proof by induction, proof by case analysis; recursion; and propositional logic.
  3. The sorts of basic data structures and algorithms encountered in an undergraduate course like CS 251, e.g. lists, trees, heaps, graphs, sorting, graph traversals, and search.

We'll briefly review important concepts as needed, but this will be a refresher and not an introduction.

In this course, we will be programming in both Rust and Haskell. As an upper-level undergraduate course, some assignments may be slightly underspecified; you may need to proactively ask questions to clarify your understanding. You are expected to test your programs before submitting, and you should ensure that every program you submit compiles without errors.

resources

Course Texts:

Our resource for learning Haskell will be the e-book Learn You a Haskell for Great Good! by Miran Lipovaca; for learning Rust we will use The Rust Programming Language by Steve Klabnik and Carol Nichols. The (optional) textbook Types and Programming Languages by Benjamin Pierce has an excellent in-depth treatment of semantics and type system; the Software Foundations series has a similar presentation of many of those topics using a proof assistant.

Discussion Forum:

The course Ed Discussion site will serve as the discussion board; all course announcements will also be posted there. In lieu of emailing the instructor or the TA with any general questions about using Haskell / Rust or assignments, please post them to the discussion board so that any other students with the same question can see the answer.

policies

Grading:

Final grades will be assigned according to the following breakdown:

Homework Assignments 45%
Project 20%
Midterm: March 8th (Tentative) 10%
Final: TBD 15%
Participation 10%

(tentative) schedule

Date Topic Notes Homework
01/08 Course Introduction + Haskell Hello HW0 assigned
01/10 Algebraic Datatypes
01/12 Inductive Datatypes + Recursive Functions HW0 Due
01/15 No Class (MLK Day) HW1 Assigned
01/17 Property-Based Testing
01/19 First-Class Functions
01/22 Parametric Polymorphism
01/24 Ad-Hoc Polymorphism (Typeclasses)
01/26 Embedded DSLS HW1 due 
01/29 Lambda Calculus + Operational Semantics HW2 assigned
01/31 Reduction strategies for the Lambda Calculus
02/02 Church Encodings
02/05 Type Systems + Type Safety
02/07 Simply Typed Lambda Calculus
02/09 Type Inference HW2 Due
02/12 Unification HW3 Assigned
02/14 Bidirectional Typing
02/16 Monads or Who left state in my functional language!?
02/19 Algebraic Effects
02/21 Demo Day: Liquid Haskell (Refinement Types)
02/23 System F HW3 Due
02/26 Scoping
02/28 Debruijn Indices
03/01 Flex Time
03/04 Flex Time
03/06 Midterm Review
03/08 Midterm  
03/18 Intro to Rust HW4 Assigned
03/20 Who left functional concepts in my systems language!?
03/22 Who left functional concepts in my systems language!?
03/25 Memory Mangagement 
03/27 Ownership
03/29 References + Borrowing HW4 Due
04/01 Big-Step Operational Semantics HW5 Assigned
04/03 Modelling the Heap
04/05 Affine + Linear Types
04/08 Subtyping
04/10 Subtyping
04/12 Gradual Typing HW5 Due
04/15 Data Abstraction HW6 Assigned
04/17 Data Abstraction
04/19 Data Abstraction
04/22 Advanced Topics (e.g. Curry Howard, Dependent Types, Coq)
04/24 Advanced Topics (e.g. Curry Howard, Dependent Types, Coq)
04/26 Course Wrap-up HW6 Due