CSE 40431
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.
| 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 |
Review of induction. NB, a simple language of numbers and Booleans. Three styles of semantics (operational, denotational, axiomatic).
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.
Formally defining the syntax and small-step operational semantics of λ. Call-by-value and call-by-name.
Large-step operational semantics, environments and closures.
Types enable compilers to catch certain kinds of programmer errors. Simply-typed NB. Programming in ML.
λ→ and its properties: it is strongly normalizing; it can't type pred or tail. PCF (= λ→ + NB + fix). Implementing a type checker and type reconstruction.
Sum and product types. (Iso)recursive types make a variety of data structures (and even an embedding of untyped λ-calculus) typable.
System F and its properties: it can type Church encodings of algebraic data types; it is strongly normalizing; type inference is undecidable.
The Hindley-Milner type system restricts System F to make type reconstruction decidable (and efficient in practice).
Semantics of a single memory cell and of ML-style references. Mutable variables in other programming languages.
Various control structures with their evaluation and typing rules: exceptions; generators; nondeterminism.
(Delimited) continuations can express a wide range of other effects, and continuation-passing style provides one way to implement them.
Presentations and conclusions.
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 |
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.
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.
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.