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.

Information

Instructor
Prof. David Chiang
Office hours MF 3–5pm
After 4/8: WF 12–1pm
326D Cushing
Teaching Assistant
Nicholas Botzer
Lectures
MWF 10:30–11:20am, 223 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)
Chailloux et al., Developing Applications with Objective Caml (free online)
Related websites
Slack #cse-40431-sp19
GitLab ND-CSE-40431 Spring 2019
Sakai SP19-CSE-40431-01

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 (2019/01/16–18)

Preliminaries

What is programming language semantics, and why does it matter? Review of Scheme (especially higher-order functions and lexical scoping).

Reading
Notes: Introduction
TAPL 1, 2
Scheme 2.1–8, 3.2
Assignment
HW 1 (due 01/25)

Week 2 (01/21–25)

Semantics

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

Reading
TAPL 3
Notes: Induction
Notes: Untyped NB
Assignment
PP 1 (due 02/01)

Functions

Week 3 (01/28–02/01)

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
Notes: Untyped λ-calculus
Notes: Data structures in λ
Notes: Recursion in λ
Assignment
HW 2 (due 02/08)

Week 4 (02/04–08)

Semantics of λ

Formally defining the syntax and small-step operational semantics of λ. Call-by-value and call-by-name.

Reading
TAPL 5.3
Notes: More about evaluation
Notes: More about equality
Assignment
HW 3 (due 02/15)

Week 5 (02/11–15)

Implementing λ

Large-step operational semantics, environments and closures.

Reading
Notes: Environments
Assignment
PP 2 (due 02/22)

Types

Week 6 (02/18–22)

Introduction to types

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

Reading
TAPL 8
OCaml 2.1
Notes: Typed NB
Assignment
HW 4 (due 03/01)

Week 7 (02/25–03/01)

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
Notes: Simply-typed λ
Notes: Type reconstruction
Assignment
PP 3 (due 03/08)

Week 8 (03/04–08)

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
OCaml 2.2
TAPL 11.6–10, 20.1–2
Notes: Algebraic data types
Assignment
HW 5 (due 03/22)

Week 9 (03/25–29)

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
Notes: System F
Assignment
HW 6 (due 03/29)

Week 10 (03/25–29)

Let-polymorphism

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

Reading
TAPL 22.7
Notes: Fragments of System F
Notes: Existential types
Assignment
Project proposal (due 04/05)

Effects

Week 11 (04/01–05)

State

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

Reading
Scheme 2.9, OCaml 3.1
TAPL 13
Notes: State
Assignment
HW 7 (due 04/12)

Weeks 12–13 (04/08–12, 04/15–17)

Control

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

Reading
OCaml 2.3
TAPL 14
Notes: Exceptions
Notes: Nondeterminism
Notes: Generators
Assignment
HW 8 (due 04/29)

Week 14 (04/24–26)

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
Notes: Continuations

Week 15 (04/29–05/01)

Conclusion

Presentations and conclusions.

Assignment
Project report (due 05/08)
Reading
Notes: Continuations continued
Notes: 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.