Doctoral Thesis Proposal - Sophia Roshal
May 13, 2026 10:00AM—11:30AM
Location:
4303 & Zoom
-
Gates and Hillman Centers
Speaker:
SOPHIA ROSHAL,
Ph.D. Student, Computer Science Department, Carnegie Mellon University
https://sophiasr.github.io/
Substructural type systems offer a principled foundation for reasoning about resource usage by controlling the structural rules of weakening, contraction, and exchange. Linear, affine, strict, and ordered types each enable distinct optimizations and semantic guarantees. However, systems restricted to a single structural discipline are often too rigid for practical programming, limiting expressiveness and preventing programs from simultaneously exploiting multiple structural properties.
This thesis develops Adjoint Types, a logically founded substructural type system based on Adjoint Logic, that supports the principled combination of multiple substructural modes within a single language. This design preserves the practical expressiveness of an unrestricted language, while still permitting mode based optimizations on the pieces of the program that allow them.
The proposal proceeds in four parts. First, we present Adjoint Natural Deduction, including both a declarative and algorithmic type system, and establish soundness and completeness with respect to a sequent calculus formulation. Second, we develop a mode inference procedure that supports mode polymorphism and eliminates the need for manual mode annotations. Third, we extend the framework with ordered modes, establishing decidability for a corresponding type system, while outlining ongoing work toward practical type-checking algorithms. Fourth, we propose generalized pattern matching in the adjoint setting, developing a logically sound approach to nested patterns via focusing and outlining extensions to support wildcards and ordered modes.
Together, these contributions establish ordered adjoint types as a logical foundation for substructural functional programming languages and logical frameworks, enabling structural properties to drive compiler optimizations and intensional program behavior without sacrificing practical usability.
Thesis Committee:
Frank Pfenning (Chair)
Jan Hoffmann
Jonathan Aldrich
Brigitte Pientka (McGill University)
Chris Martens (Northeastern University)
In-person and Zoom
Contact
Matt Stewart