Zoe Paraskevopoulou

Me

About me

I am an Assistant Professor at the School of Electrical and Computer Engineering at National Technical University of Athens (since September 2024). My research focuses on developing techniques and tools that enhance the reliability and trustworthiness of software systems.

I obtained my PhD from Princeton University, advised by Andrew Appel, where I worked on certified compilation of functional languages. You can find my CV here.

Publications

Michael Fitzgibbons, Zoe Paraskevopoulou, Noble Mushtak, Michelle Thalakottur, Jose Sulaiman Manzur, and Amal Ahmed. RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly. ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI), June 2024.

Dxo, Mate Soos, Zoe Paraskevopoulou, Martin Lundfall and Mikael Brockman. hevm, a Fast Symbolic Execution Framework for EVM Bytecode. (tool paper) 36th International Conference on Computer Aided Verification (CAV), July 2024.

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

Service