Arthur Azevedo de Amorim

Arthur Azevedo de Amorim is an Assistant Professor in the Department of Computer Science at the Golisano College of Computing and Information Sciences, Rochester Institute of Technology (RIT). He holds a Ph.D. from the University of Pennsylvania, advised by Benjamin Pierce and Cătălin Hrițcu, with postdoctoral work at Boston University and Carnegie Mellon University. His undergraduate studies were at the University of Campinas (Unicamp) and École Polytechnique (Polytechnique).

His research focuses on improving software security through formal verification, programming languages, and type systems. Key areas include cryptographic protocols, compartmentalization techniques for secure compilation, and formal semantics. Notable projects include Cryptis (separation logic for cryptographic protocols) and SECOMP (formally verified compartmentalizing compiler).

Arthur teaches courses such as Programming Language Concepts and Programming Language Theory at RIT. He actively contributes to open-source projects like the Coq proof assistant and maintains the Deriving library for generic instance generation in Coq.

His recent work emphasizes formal methods for secure systems, with publications in top venues like POPL, CCS, and ICALP. He advises several graduate and undergraduate students on topics ranging from formal verification to programming language design.