Resource Aware Programming Languages Course ID 15714 Description Resource use—the amount of time, memory, and energy a program requires for its execution—is one of the central subjects of computer science. Nevertheless, resource use traditionally does not play a central role in programming-language concepts, such as operational semantics, type systems, and program logics. This course revisits these concepts to model and analyze resource use of programs in a compositional and mathematically-precise way. The emphasis is on practical, type-based techniques that automatically inform programmers about the resource use of their code. We first study such techniques for functional programs and then develop generalizations to imperative, probabilistic, and concurrent programs. Key Topics Recurrence relations Amortized analysis and the potential method Type systems and type inference Operational semantics Cost semantics for parallel and sequential evaluation Substructural type systems Linear automatic amortized resource analysis Automatic amortized resource analysis for higher-order programs Polynomial amortized resource analysis Type inference for automatic amortized resource analysis Resource Aware ML Probabilistic programming Weakest pre-expectation calculus Session types Required Background Knowledge functional programming; basic PL theory (as covered by 15-312 or 15-814); some experience with the analysis of algorithms; basic math skills (combinatorics, proofs, probabilities, etc.) Course Relevance Ph.D. students, Master's students, and undergraduate students who took 15-312 Course Goals 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 Learning Resources Resource Aware ML (https://raml.co) Assessment Structure Homework 60%, Participation 15%, Project 25% Extra Time Commitment n/a Course Link https://www.cs.cmu.edu/~janh/courses/ra20/
