Doctoral Speaking Skills Talk - Sophia Roshal
April 21, 2026 9:30AM—10:30AM
Location:
In Person
-
Traffic21 Classroom, Gates Hillman 6501
Speaker:
SOPHIA ROSHAL,
Ph.D Student
Computer Science Department
Carnegie Mellon University
https://sophiasr.github.io/
There has been growing interest in programming languages in which types control resource usage. In most languages, types only track the types of expressions, but they do not capture how the underlying resources are used. Substructural type systems on the other hand track usage explicitly. Linear types require that each resource is used exactly once, affine types require that it is used at most once, and strict types require that it is used at least once. The “standard” types which do not restrict resource usage we call unrestricted in this setting.
These distinctions have practical use cases. As just one example, languages such as Rust use an affine type system to enforce thread safety by ensuring that resources cannot be accessed more than once. The same restriction of single use can be used to implement memory-reuse compiler optimizations that can immediately re-use the memory of a value that we know can never be read again.
In practice, most programs are not purely linear, affine, strict, or unrestricted, but instead have pieces of programs at different modes. This talk introduces Adjoint Types, a type system for a functional programming language that allows these modes to coexist within the language. This allows us to exploit the benefits of linear, affine, strict, and unrestricted typing while retaining the flexibility of a programming language with only unrestricted types.
Presented in Partial Fulfillment of the CSD Speaking Skills Requirement
For More Information:
matthewstewart@cmu.edu