6001 Gates Hillman Center
School of Computer Science
Carnegie Mellon University
5000 Forbes Ave
Pittsburgh, PA 15213
ca...@cs.cmu.edu
http://www.carloangiuli.com/blog
(412) 268-1964 (office)
I am a first-year Ph.D. student in the Computer Science Department at Carnegie Mellon University, advised by Robert Harper. I previously studied at Indiana University Bloomington, where I received a B.S. in Mathematics and in Computer Science.
I am interested in programming language theory, applied logic, and the parts of mathematics not involving numbers.
I am currently working on the homotopy type theory project, which interprets Martin-Löf type theory in a homotopical (or, higher categorical) setting, by allowing non-trivial higher-dimensional structure in the type theory.
I am also working with John Harrison at Intel on projects related to the formal semantics of (x86) machine code, and in particular, semantics-preserving machine code transformations. More details, hopefully, forthcoming.