Ph.D. Student Recruiting
October 2024
Carlo Angiuli
I am a second-year assistant professor at Indiana University looking to recruit two Ph.D. students to start in Fall 2025. My research interests are in the theory and practice of (full-spectrum) dependent types, a topic you can read about in the draft book Principles of Dependent Type Theory that I am coauthoring with Daniel Gratzer.
I am particularly interested in topics such as:
- homotopy type theory and its applications to verified functional programming (e.g., Internalizing Representation Independence with Univalence and Homotopical patch theory),
- improving the usability of dependent types through carefully-designed core language features (e.g., Controlling unfolding in type theory, which was added to Agda 2.6.4, and various experiments in the redtt and cooltt proof assistants), and
- reconsidering the syntax of type theory, particularly in its treatment of equality (e.g., XTT and Cartesian cubical type theory).
My grant proposal on Univalent Verification of Parameterized Structures was recently funded by the Air Force Office of Scientific Research for $449,387 over three years, and most of this money is earmarked to support Ph.D. students. If any of the above topics sound interesting to you, please send me an email at cangiuli@iu.edu and/or apply! (Please ensure that your email would make significantly less sense if “dependent types” were substituted with “machine learning”—I receive many mass emails that fail this test.)