CS 456: Programming Languages

LWSN B134 12:00-13:15 TTh



Ben Delaware

bendy at purdue.edu

Office Hours: Tuesday 2:30-4:00, LWSN 2116M

Teaching Assistant:

Shivaram Gopal

gopals at purdue.edu

Office Hours: Monday+Wednesday 4:00-5:00, HAAS 264

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 modularity. Work in the course involves exploring programming languages and features both as a user (by writing programs in those languages), as a language designer (by implementing interpreters for those languages), and as a scholar (by proving mathematical properties of them). We will investigate approaches to modularity such as data abstraction, inheritance, and polymorphism independent of their realization in any particular language. The course will also offer a 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 efficient and correct programs in a functional programming language, Haskell.
  2. Precisely formulate the syntax and runtime behavior of a programming language.
  3. Specify different notions of type safety for a programming language and reason about a programming language's semantics via mathematical induction.
  4. Distinguish between different approaches to modularity and abstraction provided by programming languages.

The course is structured into five sections, the first four of which roughly align with these topics. The final section will consider the realization of some of these ideas in Rust, a modern systems programming language.


Course Text:

Types and Programming Languages . Benjamin Pierce.

Learn You a Haskell for Great Good! . Miran Lipovaca.

Discussion Forum:

The course piazza 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 Coq or assignments, please post them to piazza so that any other students with the same question can see the answer.



Final grades will be assigned according to the following breakdown:

Homework Assignments 40%
Midterm: March 6th (Tentative) 20%
Final: May 1st 30%
Participation 10%

Homework Submission:

Homeworks are to be submitted via turnin by 9PM on their assigned due date. You receive two courtesy late days for the semester. Once you have used both those days, any late homeworks will not be accepted. While students can discuss assignments at a high-level, each student should produce the solutions they submit individually. A more detailed discussion of academic honesty can be found here.


Note: This schedule is preliminary; it will likely change over the course of the semester to adapt to reality.

Date Topic Notes / Homework
01/09 Introduction
Functional Programming in Haskell
01/11 Basic Data Structures LYaH Chapter 2
01/16 Inductive Data Structures LYaH Chapter 8
01/18 Recursion + Higher Order Functions LYaH Chapters 4, 5
01/23 Parametric Polymorphism LYaH Chapters 3, 6
Homework 1 (Due 2/2)
01/25 Ad-hoc Polymorphism using Type Classes
Embedded Domain Specific Languages
LYaH Chapter 8
01/30 Purity + Reasoning about Programs Equationally
02/01 Free Theorems and Haskell Revue Theorems for Free!
Dynamic Semantics
02/06 Concrete and Abstract Syntax; Binding scope TAPL Chapters 3.2; 4.1; 5.1
Homework 2 (Due 2/16)
02/08 Operational Semantics TAPL Chapters 3.4; 3.5; 4.2
02/13 Evaluation Strategies TAPL Chapter 5
02/15 Imperative Languages; Monads Winskel, Chapter 2
LYaH Chapter 12
02/20 Cultural Enrichment: Equational Reasoning in Coq SF Chapter 5
02/22 Monads, continued LYaH Chapter 13
Homework 3 (Due 3/6)
02/27 Non-local control flow; Delimited Continuations An argument against call/cc

Go-to statement
considered harmful
03/01 Meta-Programming via Partial Evaluation A tutorial on partial
03/06 Reasoning about programs inductively;
Midterm Review
Sample Midterm
03/08 Midterm
Static Semantics
03/13 Spring Break!!
03/15 Spring Break!!
03/20 Type System Basics TAPL Chapter 9
03/22 Type Checking and Type Inference TAPL Chapter 22
03/27 Type Checking and Type Inference, Continued TAPL Chapter 22
Homework 4 (Due 4/6)
03/29 Language Metatheory: Proving Type Safety TAPL Chapter 3
TAPL Chapter 8
TAPL Chapter 9
04/03 Polymorphic Lambda Calculus TAPL Chapter 23
04/05 Dynamic Typing
Modularity and Abstraction
04/10 Abstract Data Types; Representation Invariants TAPL Chapter 24
04/12 Representation Independence
04/17 Objects vs. ADTs On Understanding
Data Abstraction,
04/19 Subtyping TAPL Chapter 15
Course Finale
04/24 Memory Safety, Affine Types, and Rust Ownership in Rust
A Taste of Linear Logic
04/26 Course Wrap-up