Arthur Azevedo de Amorim

About me

I am a graduate student in the Computer and Information Science department at the University of Pennsylvania since 2011. I work with Benjamin Pierce. You can find my CV here.

Research Interests

My main research area is programming languages and verification. I was involved in the project of SAFE, a clean-slate computer environment aimed at security and correctness, helping with its design and specification. I am currently working on bringing some of the hardware tagging infrastructure that we developed for SAFE to more conventional processor designs, formally verifying that the mechanism can be used for enforcing interesting security policies. for I am also a proud member of the PL Club at Penn.

Publications and Talks

Cătălin Hriţcu, Leonidas Lampropoulos, Antal Spector-Zabusky, Arthur Azevedo de Amorim, Maxime Dénès, John Hughes, Benjamin C. Pierce, and Dimitrios Vytiniotis. Testing Noninterference, Quickly. Special Issue of Journal of Functional Programming (JFP) for ICFP 2013. 26:e4 (62 pages), April 2016. An earlier version of this paper appeared in ICFP 2013. (arxiv).

Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Cătălin Hriţcu, David Pichardie, Benjamin C. Pierce, Randy Pollack and Andrew Tolmach. A Verified Information-Flow Architecture. Journal of Computer Security (JCS); Special Issue on Verified Information Flow Security, 24(6):689--734, December 2016. (An earlier version of this work appeared POPL 2014. (arxiv, Slides)

Arthur Azevedo de Amorim, Justin Hsu, Marco Gaboardi, Emilio Jesús Gallego Arias. Type-checking Linear Dependent Types. TYPES 2014 Paris. (Slides)

Arthur Azevedo de Amorim, Marco Gaboardi, Emilio Jesús Gallego Arias, and Justin Hsu. Really naturally linear indexed type-checking In Proceedings of Implementation of Functional Languages (IFL), Boston, Massachusetts, USA, 2014. (arXiv)

Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Cătălin Hrițcu, Benjamin C. Pierce, Antal Spector-Zabusky, Andrew Tolmach. Micro-Policies: Formally Verified, Tag-Based Security Monitors. In 36th IEEE Symposium on Security and Privacy, San Jose, California, USA, 2015 (Extended Version, Slides)

Yannis Juglaret, Cătălin Hrițcu, Arthur Azevedo de Amorim, Benjamin C. Pierce. Beyond Good and Evil: Formalizing the Security Guarantees of Low-Level Compartmentalization. To appear in 29th IEEE Symposium on Computer Security Foundations (CSF) (arXiv)

Arthur Azevedo de Amorim. Binding Operators for Nominal Sets. In MFPS 2016 (PDF, DOI: 10.1016/j.entcs.2016.09.029)

Arthur Azevedo de Amorim, Ikram Cherigui, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata. A Semantic Account of Metric Preservation. In POPL 2017 (PDF)


Arthur Azevedo de Amorim, Benjamin C. Pierce. Alpha is for Address! (PDF)


I also have a blog about the Coq proof assistant


You can reach me at aarthurAcisDupennDedu. Or send me a letter:

Arthur Azevedo de Amorim
3330 Walnut Street
CIS Dept., Levine Hall 302
Philadelphia, PA 19104-3409
United States