Publications
For a full list, see my Google Scholar profile.
Under Submission
Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)
Zoe Paraskevopoulou
Act: From EVM Bytecode to Machine-Checked Reasoning for Smart Contracts
Zoe Paraskevopoulou, Lefteris Lazaropoulos, Anja Petković Komel, Sophie Rain, and Alexis Terry
Conference Papers
RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly
Michael Fitzgibbons, Zoe Paraskevopoulou, Noble Mushtak, Michelle Thalakottur, Jose Sulaiman Manzur, and Amal Ahmed
PLDI 2024
hevm, a Fast Symbolic Execution Framework for EVM Bytecode (tool paper)
Dxo, Mate Soos, Zoe Paraskevopoulou, Martin Lundfall, and Mikael Brockman
CAV 2024
Computing Correctly with Inductive Relations
Zoe Paraskevopoulou, Aaron Eline, and Leonidas Lampropoulos
PLDI 2022
Compiling with Continuations, Correctly
Zoe Paraskevopoulou and Anvay Grover
OOPSLA 2021
Compositional Optimizations for CertiCoq
Zoe Paraskevopoulou, John M. Li, and Andrew W. Appel
ICFP 2021
Closure Conversion is Safe for Space
Zoe Paraskevopoulou and Andrew Appel
ICFP 2019
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
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
ESOP 2019
Generating Good Generators for Inductive Relations
Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin Pierce
POPL 2018
A Type Theory for Incremental Computational Complexity with Control Flow Changes
Ezgi Çiçek, Zoe Paraskevopoulou, and Deepak Garg
ICFP 2016
Foundational Property-Based Testing
Zoe Paraskevopoulou, Cătălin Hriţcu, Maxime Dénès, Leonidas Lampropoulos, and Benjamin C. Pierce
ITP 2015
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
Theses
Verified Optimizations for Functional Languages
PhD Thesis, Princeton University. Advised by Andrew Appel
Self-Adjusting Computation for CostIt
Master's Thesis, ENS Paris-Saclay. Advised by Deepak Garg
A Coq Framework For Verified Property-Based Testing
Diploma Thesis, National Technical University of Athens. Advised by Cătălin Hriţcu