I am a postdoctoral researcher at CMU working with Anupam Datta and Matt Fredrikson. I am interested in programming languages, formal verification, and computer security.
I am from Campinas, SP, Brazil. I pursued my Ph.D. studies at the University of Pennsylvania, under the supervision of Benjamin Pierce and co-advised by Cătălin Hrițcu. Prior to that, I was a student at Unicamp and at Polytechnique. I am one of the authors of Software Foundations, an introductory textbook to the Coq proof assistant. I also have a blog about Coq.
February 2018 A draft of our new paper on secure compilation, When Good Components Go Bad, is out on arxiv. Check also the accompanying Coq formalization on GitHub.
January 2018 Our paper The Meaning of Memory Safety (arxiv) was accepted at POST 2018.
September 2017 I served on the external review committee for PLDI 2018.
Check also my DBLP and Google Scholar pages.
The Meaning of Memory Safety. Arthur Azevedo de Amorim, Catalin Hritcu, and Benjamin C. Pierce. In Proceedings of POST 2018, part of ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, pages 79--105, 2018. [ http ]
A methodology for micro-policies. Arthur Azevedo de Amorim. PhD thesis, University of Pennsylvania, 2017. [ .pdf ]
A semantic account of metric preservation. Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 545--556, 2017. [ arxiv ]
Binding Operators for Nominal Sets. Arthur Azevedo de Amorim. Electr. Notes Theor. Comput. Sci., 325:3--27, 2016. [ http ]
A verified information-flow architecture. 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. Journal of Computer Security, 24(6):689--734, 2016. [ DOI | arxiv ]
Testing noninterference, quickly. 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. J. Funct. Program., 26:e4, 2016. [ DOI | arxiv ]
Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation. Yannis Juglaret, Cӑtӑlin Hrițcu, Arthur Azevedo de Amorim, Boris Eng, and Benjamin C. Pierce. In IEEE 29th Computer Security Foundations Symposium, CSF 2016, Lisbon, Portugal, June 27 - July 1, 2016, pages 45--60, 2016. [ DOI | arxiv ]
Micro-Policies: Formally Verified, Tag-Based Security Monitors. Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Cӑtӑlin Hrițcu, Benjamin C. Pierce, Antal Spector-Zabusky, and Andrew Tolmach. In 2015 IEEE Symposium on Security and Privacy, SP 2015, San Jose, CA, USA, May 17-21, 2015, pages 813--830, 2015. [ DOI | slides | full version ]
Really Natural Linear Indexed Type Checking. Arthur Azevedo de Amorim, Marco Gaboardi, Emilio Jesús Gallego Arias, and Justin Hsu. In Proceedings of the 26th 2014 International Symposium on Implementation and Application of Functional Languages, IFL '14, Boston, MA, USA, October 1-3, 2014, pages 5:1--5:12, 2014. [ DOI | arxiv ]
A verified information-flow architecture. 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. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 165--178, 2014. [ DOI | slides ]
Testing noninterference, quickly. Cӑtӑlin Hrițcu, John Hughes, Benjamin C. Pierce, Antal Spector-Zabusky, Dimitrios Vytiniotis, Arthur Azevedo de Amorim, and Leonidas Lampropoulos. In ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013, pages 455--468, 2013. [ DOI ]
Extensional Structures: A Coq library of finite data structures that support extensional equality.
Micro-policies: A programming model for tag-based security policies formalized in Coq.
Coq utils: A small library of Coq utilities, including a formalization of nominal sets.