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

category	points
Homework assignments	8×15
Programming projects	3×30
Final project/paper	60
Participation	30
Total	300

grade	points	grade	points	grade	points
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.