CSE 40431

Programming Languages

Introduction to the theory of programming languages. How to define programming languages using operational semantics and type systems, and how to prove things about them. Starting with the lambda calculus as a core, a simple programming language is built up, with higher-order functions and lexical scope; algebraic data types, polymorphic types, and type inference; state and control. Students will also gain experience with functional programming and writing interpreters.

The information below is from the last offering of the course in Spring 2019. Details are subject to change. Your input is welcome!

Information

Instructor
Prof. David Chiang
Teaching Assistants
Colin McDonald
Lectures
MWF 11:30am–12:20pm, 125 DeBartolo
Prerequisites
Programming Paradigms (CSE 30332) recommended but not required
Theory of Computing (CSE 30151) recommended but not required
Textbooks
Pierce, Types and Programming Languages (free via library)
Dybvig, The Scheme Programming Language, 4th ed. (free online)
OCaml documentation

Requirements and Grading

categorypoints
Homework assignments8×15
Programming projects3×30
Final project/paper60
Participation30
Total300
gradepointsgradepointsgradepoints
A− 270–279 A 280–300
B− 240–249 B 250–259 B+ 260–269
C− 210–219 C 220–229 C+ 230–239
D 180–209
F 0–179

Schedule

Week 1 (2022/08/24–26)

Preliminaries

What is programming language semantics, and why does it matter? Review of induction.

Reading
Introduction
Induction
TAPL 1, 2
Assignment
HW 1 (due 09/02)

Week 2 (08/29–09/02)

Semantics

NB, a simple language of numbers and Booleans. Three styles of semantics (operational, denotational, axiomatic).

Reading
TAPL 3
Syntax of NB
Semantics of NB
Assignment
PP 1 (due 09/09)

Functions

Week 3 (09/05–09/09)

Scheme

Review of Scheme (especially higher-order functions and lexical scoping).

Reading
Scheme 2.1–8, 3.2
Notes on Scheme
Assignment
HW 2 (due 09/16)

Week 4 (09/12–16)

Untyped λ-calculus

The λ-calculus, the world's oldest programming language. How it works and how to program in it. Encoding numbers, Booleans, and other data structures. Recursion.

Reading
TAPL 5.1–2
Untyped λ-calculus
Data structures in λ
Recursion in λ
Assignment
HW 3 (due 09/23)

Week 5 (09/19–23)

Semantics of λ

Small-step and big-step operational semantics of λ. Environments and closures.

Reading
TAPL 5.3
Semantics of λ
Environments
More about evaluation [G]
More about equality [G]
Assignment
PP 2 (due 09/30)

Types

Week 6 (09/26–30)

Types and ML

Types enable compilers to catch certain kinds of programmer errors. Simply-typed NB. Programming in ML.

Reading
TAPL 8
Notes on OCaml and links therein
Typed NB
Assignment
HW 4 (due 10/07)

Week 7 (10/03–07)

Simply typed λ-calculus

λ and its properties: it is strongly normalizing; it can't type pred or tail. PCF (= λ + NB + fix). Implementing a type checker and type reconstruction.

Reading
TAPL 9, 10, 11.1–5, 11.11, 22.1-6
Simply-typed λ
Type reconstruction
Assignment
PP 3 (due 10/14)

Week 8 (10/10–14)

Algebraic data types

Sum and product types. (Iso)recursive types make a variety of data structures (and even an embedding of untyped λ-calculus) typable.

Reading
TAPL 11.6–10, 20.1–2
Sum and product types
Recursive types
Assignment
HW 5 (due 10/28)

Week 9 (10/24–28)

Universal types

System F and its properties: it can type Church encodings of algebraic data types; it is strongly normalizing; type inference is undecidable.

Reading
TAPL 23
System F
TAPL 24 [G]
Existential types [G]
Assignment
HW 6 (due 11/04)

Week 10 (10/31–11/04)

Let-polymorphism

The Hindley-Milner type system restricts System F to make type reconstruction decidable (and efficient in practice).

Reading
TAPL 22.7
Fragments of System F
Assignment
Project proposal (due 11/11)

Effects

Week 11 (11/07–11)

State

Semantics of a single memory cell and of ML-style references. Mutable variables in other programming languages.

Reading
Scheme 2.9, OCaml on arrays and refs
TAPL 13
State
Assignment
HW 7 (due 11/18)

Weeks 12–13 (11/14–18, 21)

Control

Various control structures with their evaluation and typing rules: exceptions; generators; nondeterminism.

Reading
TAPL 14
Exceptions
Nondeterminism
Generators
Assignment
HW 8 (due 12/02)

Week 14 (11/28–12/02)

Continuations

(Delimited) continuations can express a wide range of other effects, and continuation-passing style provides one way to implement them.

Reading
Scheme 3.3–4
Continuations

Week 15 (12/05–07)

Conclusion

Presentations and conclusions.

Assignment
Project report (due 05/08)
Reading
Continuations continued
Conclusion

Policies

Honor Code

Students in this course are expected to abide by the Academic Code of Honor Pledge: “As a member of the Notre Dame community, I will not participate in or tolerate academic dishonesty.”

The following table summarizes how you may work with other students and use print/online sources:

Resources Solutions
Consulting allowed not allowed
Copying cite not allowed
See the CSE Guide to the Honor Code for definitions of the above terms.

If an instructor sees behavior that is, in his judgement, academically dishonest, he is required to file either an Honor Code Violation Report or a formal report to the College of Engineering Honesty Committee.

Late Submissions

In the case of a serious illness or other excused absence, as defined by university policies, coursework submissions will be accepted late by the same number of days as the excused absence. Otherwise, you may submit part of an assignment on time for full credit and part of the assignment late with a penalty of 30% per week (that is, your score for that part will be ⌊0.7 s⌋, where s is your raw score and t is the possibly fractional number of weeks late). No part of the assigment may be submitted more than once. No work may be submitted after the final project due date.

Students with Disabilities

Any student who has a documented disability and is registered with Disability Services should speak with the professor as soon as possible regarding accommodations. Students who are not registered should contact the Office of Disability Services.