معرفی
Carlo Angiuli is an Assistant Professor of Computer Science at the Luddy School of Indiana University. He is a leading researcher in type theory, with a focus on its applications to programming language design and logic. His work bridges theoretical foundations and practical implementations, particularly through dependent types, proof assistants, and homotopy type theory.
His research interests include:
- Type Theory (foundational systems for programs and proofs)
- Programming Language Foundations (formal semantics and reasoning)
- Homotopy Type Theory (higher-dimensional structures)
- Dependent Types (expressive type systems)
- Proof Assistants (formal verification tools)
- Computational Logic (algorithmic reasoning)
Angiuli actively contributes to the programming languages community as a POPL Program Committee member and co-author of a forthcoming textbook on dependent type theory. His students include Johnson He, Huang Xu, Kelton OBrien, and Ian Ray, who joined in Fall 2025. He has received significant recognition, including the Best Paper Award at FSCD 2019 and the School of Computer Science Distinguished Dissertation Award from Carnegie Mellon University. His current work explores advanced type-theoretic frameworks and their implementation in proof assistants like the red* family of tools.
Scientific awards:
- Best Paper Award, FSCD 2019 (Junior Researchers category)
- School of Computer Science Distinguished Dissertation Award, Carnegie Mellon University
He teaches courses such as Modern Dependent Types (CSCI-B619), Programming Language Foundations (CSCI-B522), and Introduction to Computer Science (CSCI-C211).
