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.

This course is planned to be offered in Spring 2019. It will join a “trilogy” of courses on programming languages, the other two being Programming Paradigms (CSE 30332) and Compilers and Language Design (CSE 40243). Whereas Paradigms is about using programming languages and Compilers is about implementing programming languages, this course is about programming language semantics, which bridges the other two by defining, in a mathematical way, what programming languages mean.

This is a very preliminary preview of the course, so you can decide whether you're interested, but more importantly, so you can give me feedback (by email or Slack) about what you'd like to change.

Information

Instructor
Prof. David Chiang
Lectures
MWF 10:30–11:20am, DeBartolo 223
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)

Requirements

Homework assignments (pencil-and-paper problems, short programming exercises)8×5%
Programming projects3×10%
Final project/paper30%

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
TAPL 1, 2
Scheme 2.1–8, 3.2
Assignment
HW 1

Week 2 (01/21–25)

Semantics

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

Reading
TAPL 3
Assignment
PP 1 (NB interpreter)

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
Assignment
HW 2

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
Assignment
HW 3

Week 5 (02/11–15)

Implementing λ

Large-step operational semantics, environments and closures. Functions in real-world programming languages.

Reading
Notes
Assignment
PP 2 (λ interpreter)

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
Assignment
HW 4

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.

Reading
TAPL 9, 10, 11.1–5, 11.11
Assignment
HW 5

Week 8 (03/04–08)

Type reconstruction

Constraint-based typing is a formulation of typing rules that lets the programmer leave types implicit, for the compiler to reconstruct.

Reading
TAPL 22.1-6
Assignment
PP 3 (type checking/inference)

Week 9 (03/18–22)

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
Assignment
HW 6

Week 10 (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. Time permitting: existential types.

Reading
TAPL 23
Assignment
HW 7

Week 11 (04/01–05)

Let-polymorphism

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

Reading
TAPL 22.7
Assignment
HW 8

Effects

During this unit, students will work on a final programming project or paper on a topic of their choice. Some class time will be set aside for students to present their work in progress.

Week 12 (04/08–12)

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

Week 13 (04/15–17, Holy Week)

Control

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

Reading
OCaml 2.3
TAPL 14
Notes

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

Week 15 (04/29–05/01)

Conclusion

Presentations and conclusions.