Resource usage—the amount of time, memory, and energy a program requires for its execution—is one of the central subjects of computer science. Nevertheless, resource usage often does not play a central role in classical programming-language concepts such as operational semantics, type systems, and program logics. The first part of the course revisits these concepts to model and analyze resource usage of programs in a compositional and mathematically-precise way. The emphasis is on practical, type-based techniques that automatically inform programmers about the resource usage of their code.

The second part of the course studies probabilistic programming languages. Such languages describe probability distributions and can be used to precisely describe and analyze probabilistic models. Probabilistic languages are for instance used in statistical modeling and to facilitate probabilistic inference. The focus of the course is on the semantics and analysis of probabilistic languages. Interestingly, the techniques from the first part can be applied to automatically analyze the expected cost and results of probabilistic programs.

The third part of the course, presents an application of automatic resource bound analysis in Nomos, a programming language for implementing digital contracts. Nomos is based on session types, which are a focus in this part. Moreover, blockchains and smart contracts are briefly covered to motivate the need for resource bounds.

Class format

Lecture and project-based

Home departments

Computer Science Department

Target audience

Ph.D. students, master's students, and undergraduate students who took 15-312 (minimum grade of B needed)

Background required

There are no official prerequisites. However, you should be familiar with the foundations of programming languages as covered by courses such as 15-312 or 15-814.

Learning objectives

Students will be able to:

• manually analyze the resource use of a program using recurrence relations and amortized analysis
• define and justify cost models for programming languages using cost semantics
• analyze and define structural and substructural type systems
• comprehend and develop type systems for deriving resource bounds
• define a semantics for probabilistic programming languages
• develop programming languages that use message-passing concurrency
• use session types to bound the cost of concurrent programs

Faculty and instructors who have taught this course in the past

Jan Hoffmann