Spring 2027 Courses

An advanced follow-on to 15-312 developing further ideas and results in the theory of programming languages.

The course covers the Istari proof assistant: its type theory and its practical use in proving theorems and reasoning about programs.

First Person is a weekly speaker series that brings the most consequential people in the startup economy into one room with students from across CMU. These are the field's leading founders, operators, CEOs, and investors, along with the researchers and builders shaping where the frontier goes next, in candid conversation about the work of starting, financing, scaling, and running a venture. It runs as two independent minis in the spring, First Person: Winter Sessions in Mini 3 and First Person: Spring Sessions in Mini 4, each with its own slate of guests. Students can take either on its own or both across the semester, and a follow-on seminar allows for a smaller case discussion with that week's guest.

This course attempts to provide a deep understanding of the issues and challenges involved in designing and implementing modern computer systems. Our primary goal is to help students become more skilled in their use of computer systems, including the development of applications and system software. Users can benefit greatly from understanding how computer systems work, including their strengths and weaknesses. This is particularly true in developing applications where performance is an issue.

Theoretical and practical aspects of building optimizing compilers that e¿ectively exploit modern architectures. The course will begin with the fundamentals of compiler optimization, and will build upon these fundamentals to address issues in state-of-the-art commercial and research machines.

In this course, we will cover applications of coding thoery in cryptography. The course would start off with some basic algebraic coding theory, and then cover some exciting applications in code-based cryptography (such as Private information retrival, MPC, Post-Quantum cryptography and such).

This seminar-based course delves into the heart of physics-based animations of solids and fluids, a key component in fields ranging from visual effects and VR to digital fashion. Central to this is solving partial differential equations (PDEs) using numerical methods, with applications extending to computational mechanics, robotic training, and 3D content creation. Combining lectures with student presentations, we will explore the simulation of various physical entities, such as rigid bodies, deformable bodies (open-source online book available, including Python and CUDA examples), shells, rods, liquids, and smoke, all the way from the discretization of the governing PDEs to the efficient implementation and evaluation of the numerical solvers. Students will acquire a thorough understanding of both classic and state-of-the-art methods of solids and fluids simulation in computer graphics. They will also gain insights into the existing challenges in enhancing and applying these methods within the broader field.

This course provides a broad perspective on AI, with a focus on foundational principles powering modern AI. This course will cover (i) machine learning and neural networks, (ii) large language models and generative AI, (iii) search and reinforcement learning, (iv) game theory and multi-agent systems, and (v) issues of bias and unfairness in AI. The material will be presented from a mathematical perspective, with assignments emphasizing implementation alongside foundational principles.

This course is broadly focused on full-stack system security and will cover the foundations of building secure systems and cryptography. During the course we will cover hardware, system software, and cryptographic primitives for building secure systems, both within the datacenter environment and in the decentralized setting. The course will focus on the cross-cutting security requirements of systems and how to bolster their security guarantees using a combination of systems and cryptographic techniques. The lectures will cover fundamental security concepts (e.g., threat models, trusted computing base), and do a deep dive into state-of-the-art attacks and defenses (e.g., speculative execution attacks). The course will span a set of hardware security topics including trusted execution environments, side-channels, hardware attacks (e.g., Meltdown, Spectre, Rowhammer), software systems such as blockchains, anonymous messaging, and secure machine learning.

In this seminar class, we will discuss state-of-the-art methods in generative AI for music and general audio (everyday sounds, speech, bioacoustics, etc.), with applications to both generation and understanding. We will examine and compare the two primary families of methods that are used in modern audio generation research: large language models applied to discrete audio tokens, and diffusion models applied to continuous audio representations. With an eye towards offering intuitive controls for music generation, we will also examine classic methods and tasks in music information retrieval such as spectral analysis, synchronization, beat detection, and transcription. Moreover, we will explore emerging topics in generative AI for music and audio such as new architectures, training data attribution, interaction, compression, multimodality, and evaluation. Finally, we will discuss the ethical and societal implications of music generation specifically, and its potential effects on music both economically and culturally. Much of the course activity will center around (1) in-class lectures and demonstrations on small scale datasets, (2) student-led discussions of research papers, and (3) an open-ended research project.

This course number is used by the department for approved alternate electives for doctoral students.

This course number is used by the department for approved alternate electives for doctoral students.

This graduate course provides an introduction to substructural logics, such as linear, ordered, affine, bunched, or separation logic, with an emphasis on their applications in computer science. This includes the design and theory of programming constructs for concurrent message-passing computation and techniques for specifying and reasoning about programming languages in the form of substructural operational semantics.

An intensive graduate course on the design and analysis of algorithms.

Textile artifacts are -- quite literally -- all around us; from clothing to carpets to car seats. These items are often produced by sophisticated, computer-controlled fabrication machinery. In this course we will discuss everywhere code touches textiles fabrication, including design tools, simulators, and machine control languages. Students will work on a series of multi-week, open-ended projects, where they use code to create patterns for modern sewing/embroidery, weaving, and knitting machines; and then fabricate these patterns in the textiles lab. Students in the 800-level version of the course will be required to create a final project which develops a new algorithm, device, or technique in the realm of textiles fabrication.

This course is an introduction to physics-based rendering at the advanced undergraduate and introductory graduate level. During the course, we will cover fundamentals of light transport, including topics such as the rendering and radiative transfer equations, light transport operators, path integral formulations, and approximations such as diffusion and single scattering. Additionally, we will discuss state-of-the-art models for illumination, surface and volumetric scattering, and sensors. Finally, we will use these theoretical foundations to develop Monte Carlo algorithms and sampling techniques for efficiently simulating physically-accurate images. Towards the end of the course, we will look at advanced topics such as rendering wave optics, neural rendering, and differentiable rendering. The course has a strong programming component, in the form of assignments through which students will develop their own working implementation of a physics-based renderer, including support for a variety of rendering algorithms, materials, illumination sources, and sensors. The course also emphasizes theoretical aspects of physics-based rendering, through weekly take-home quizzes. Lastly, the course includes a final project, during which students will select and implement some advanced rendering technique, and use their implementation to produce an image that is both technically and artistically compelling. The course will conclude with a rendering competition, where students submit their rendered images to win prizes.

This course number is used for scheduling distinguished lectures offered throughout the semester.

This course number is for registering for reading and research while working on research and your dissertation.

The course number should be used for registering units for internships.