Arthur Azevedo de Amorim
CertiCoq | A verified compiler for Coq
CertiCoq | A verified compiler for Coq
I am a formal verification research engineer at Ethereum Foundation . I work on building open source tools that use formal verification techniques to provide strong guarantees about the correctness of smart contracts. I obtained my PhD from Princeton University, working with Prof. Andrew Appel on verified compilation of functional languages. You can find my CV here .
Zoe Paraskevopoulou, Aaron Eline, and Leonidas Lampropoulos. Computing correctly with inductive relations. ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI), June 2022.
Zoe Paraskevopoulou and Anvay Grover. Compiling With Continuations, Correctly. ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), October 2021.
Arthur Azevedo de Amorim
CertiCoq | A verified compiler for Coq
CertiCoq | A verified compiler for Coq