About me

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.

News

• I will be participating in the Dagstuhl Seminar Secure Compilation in November 2021.
• I defended my PhD Thesis on October 30th 2020!
• I received a CI Fellowship to work with Prof. Amal Ahmed on language interoperability on top of WebAssembly.
• I received a Siebel Scholar Award after being nominated by the Princeton CS department.
• I will be participating participating in the panel Research in Functional Programming at PLMW@ICFP’19.
• I will be participating in the Dagstuhl Seminar Secure Compilation in May 2018.
• I was interviewed for People of Programming Languages@POPL’18.

Talks

• [August 23rd 2021] Compositional Optimizations for CertiCoq, ICFP 2021 (video)
• [December 10th 2020] CertiCoq: Compositional verification in Practice, Invited Lecture @ CMSC631, University of Maryland
• [November 24th 2020] Compositional Optimizations for CertiCoq, POPV Seminar @ Boston University
• [October 30th 2020] Verified Optimizations for Functional Languages, PhD Thesis Defense, Princeton University
• [October 20th 2020] Invited lecture on CertiCoq @ Advanced Coq Programming, Saarland University
• [December 2nd 2019] CertiCoq: Current and Future Directions, NU PRL @ Northeastern University
• [August 19th 2019] Closure Conversion is Safe for Space, ICFP 2019
• [June 2nd 2019] Closure Conversion is Safe for Space, DeepSpec @ PLDI 2019
• [Sept 7th 2018] Layered DSLs for Verified Cryptography, End-of-internship talk, MSR Redmond
• [Jan 12th 2018] Generating Good Generators for Inductive Relations, POPL 2018

Publications

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.

Zoe Paraskevopoulou, John M. Li, and Andrew W. Appel. Compositional Optimizations for CertiCoq. ACM SIGPLAN International Conference on Functional Programming (ICFP), August 2021. paper, Coq artifact

Zoe Paraskevopoulou and Andrew Appel. Closure Conversion is Safe for Space. ACM SIGPLAN International Conference on Functional Programming (ICFP), August 2019. paper, slides, Coq development

Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy. Meta-F* : Proof Automation with SMT, Tactics, and Metaprograms. ESOP 2019. paper

Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin Pierce. Generating Good Generators for Inductive Relations. In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2018. paper, slides

Ezgi Çiçek, Zoe Paraskevopoulou, and Deepak Garg. A type theory for incremental computational complexity with control flow changes. ACM SIGPLAN International Conference on Functional Programming (ICFP), September 2016. paper, appendix with proofs

Zoe Paraskevopoulou, Cătălin Hriţcu, Maxime Dénès, Leonidas Lampropoulos, and Benjamin C. Pierce. Foundational Property-Based Testing. In 6th International Conference on Interactive Theorem Proving (ITP), August 2015. paper, slides

Theses

PhD Thesis
Verified Optimizations for Functional Languages, Advised by Andrew Appel
Thesis

Master’s Thesis
Self-Adjusting Computation for CostIt, Advised by Deepak Garg
Thesis, Slides

Diploma Thesis
A Coq Framework For Verified Property-Based Testing, Advised by Cătălin Hriţcu
Thesis, Slides

Workshop Papers

Enabling Safe Shared-Memory Interoperability in WebAssembly. Michael Fitzgibbons, Zoe Paraskevopoulou, Noble Mushtak, Amal Ahmed. HOPE 2022.

ML as a Tactic Language, Again. Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Cătălin Hriţcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, and Nikhil Swamy. ML 2018.

CertiCoq: A verified compiler for Coq (Extended Abstract). Abhishek Anand, Andrew Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau, and Matthew Weaver. CoqPL 2017.

Making our Own Luck: A Language for Random Generators (Extended Abstract). Leonidas Lampropoulos, Benjamin C. Pierce, Cătălin Hriţcu, John Hughes, Zoe Paraskevopoulou and Li-yao Xia. PPS 2016

A Coq Framework For Verified Property-Based Testing (Extended Abstract). Zoe Paraskevopoulou, Cătălin Hriţcu, Maxime Dénès, Leonidas Lampropoulos and Benjamin C. Pierce. CoqPL 2015.

QuickChick: Property-Based Testing for Coq. Maxime Dénès, Cătălin Hriţcu, Leonidas Lampropoulos, Zoe Paraskevopoulou and Benjamin C. Pierce. The 6th Coq Workshop. July 2014.

Students

Anvay Grover, Senior Thesis, Fall 2019/Spring 2020
Implementation and Verification of the CPS Transformation of the CertiCoq Compiler, co-advised with Prof. Andrew Appel

Katja Vassilev, Senior Thesis, Fall 2018/Spring 2019
Implementation and Verification of the Dead Parameter Elimination Optimization of the CertiCoq Compiler, co-advised with Prof. Andrew Appel

Internships

• Facebook, June - August 2019
  Provided a Rust backend for Fiat-crypto.
• Microsoft Research, Redmond, June - August 2018
  Excited to continue working on F*!
• Microsoft Research, Redmond, June - August 2017
  Excited to be working with Jonathan Protzenko and Nikhil Swamy on F* native tactic compilation.
• Max Planck Institute of Software Systems, March - August 2015
  Advised by Deepak Garg and worked on incremental computation for CostIt.
• INRIA Paris, April - September 2014
  Advised by Cătălin Hriţcu and had the opportunity to start working on QuickChick.

Service

• Program Committee, PLDI 2023
• Program Committee, PEPM 2022
• Workshops co-chair, ICFP 2022
• Program Committee, CPP 2022
• Workshops co-chair, ICFP 2021
• Program Committee, PriSC 2021
• Program Committee, TFP 2020
• Program Committee, ML 2019
• External Review Committee, ICFP 2019
• Program Committee, TyDe 2018
• Program Committee, OCaml 2017
• Artifact Evaluation Committee, POPL 2017