CS 456: Programming Languages
LWSN 1106 |
10:30a-11:20a MWF |
|
about
Instructor:
bendy at purdue.edu
Office Hours: Mondays 2:00-3:30p in LWSN 2116M
Teaching Assistant:
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:
- Write programs in two languages with
state-of-the-art type systems, Rust and
Haskell.
- Compare and contrast different
language-provided abstractions, including
ad-hoc and parametric polymorphism,
user-defined data types, and static and
dynamic memory safety.
- Precisely formulate the syntax and runtime
behavior of a programming language.
- 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:
- Programming in an imperative language, e.g. Java / C / Python, etc.
- 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.
- 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 |
|
|
|