ECE 69500 - Types and Programming Languages

Course Details

Lecture Hours: 3 Credits: 3

Areas of Specialization:

  • Computer Engineering

Counts as:

Normally Offered:

Each Spring

Campus/Online:

On-campus only

Requisites by Topic:

There are no prerequisites for the course. This is an introductory graduate course on programming languages. However, a strong background and understanding of topics in discrete mathematics, such as sets, relations, functions, sequences, propositional logic, and various forms of mathematical induction will be helpful for succeeding in this course. It is also preferable that students are comfortable with LaTeX because students are encouraged to typeset their answers to assignments in LaTeX for submission via PDF. However, we will accept handwritten neatly, scanned PDF submissions.

Catalog Description:

This is an introductory course on the mathematical foundations of programming languages. The central organizing principle of the content in this course is around the identification of language features with types. The theory of programming languages, therefore, reduces to the theory of type systems. Type theory is a comprehensive foundational theory of computation, and also corresponds (in a way that can be made mathematically precise) to the vernacular of logic. The course is about the dual interpretations of type theory as programming and as logic, and about the interplay between those interpretations.

Required Text(s):

  1. Practical Foundations for Programming Languages , Second Edition , Harper, Robert , Cambridge University Press , 2016 , ISBN No. 9781316576892
  2. Types and Programming Languages , First Edition , Pierce, Benjamin C. , Cambridge University Press , 2002 , ISBN No. 9780262162098

Recommended Text(s):

None.

Learning Outcomes

A student who successfully fulfills the course requirements will have demonstrated an ability to:

  • Define and formalize the abstract syntax, static semantics, and dynamic semantics of a programming language with fundamental data types, such as sums and products, polymorphic and abstract types, and recursive types.
  • Use such formalisms to prove type safety via progress and preservation theorems.
  • Relate fundamental data types to their corresponding features in common programming languages like Java, C/C++, Rust, etc.
  • Recognize and avoid common fallacies in proofs and language design; and critique programming languages and language constructs based on mathematical properties they may or may not satisfy.
  • Appreciate the deep philosophical and mathematical underpinnings of programming language design.

Lecture Outline:

Weeks Major Topics
1 Introduction to Types, Type Systems, and Language Design Review Mathematical; Preliminaries; Abstract Syntax and Inductive Definitions
2 Simply-Typed Lambda Calculus Statics; Substitution, Weakening
3 Dynamics (Small-step Operational Semantics); Type Safety (Progress and Preservation); Big-step Operational Semantics
4 Functions (System T) and Definability; Products and Sums
5-6 Parametric Polymorphism and System F; Existential Types; Data Abstraction; Abstraction Theorem
7 Types and Propositions; Free Theorems; Curry-Howard Isomorphism
8 PCF and Recursive Types; Higher Kinds
9 Mutable State and Effects; Modernized Algol; Assignables and References
10 Control Stacks, Exceptions, and Continuations
11 Subtyping; Featherweight Java
12 Concurrency and Distribution
13 Linear Logic; Linear and Affine Types
14 Dynamic Types; Gradual Types
15 Miscellaneous Topics: Substructural Logic, Modal Logic, Incorrectness Logic

Assessment Method:

Homework & presentations (10.2024)