Me

About me

I am a postdoctoral researcher at Northeastern University working with Prof. Amal Ahmed on language interoperability. Before that, I was a PhD student at Princeton University, working with Prof. Andrew Appel on verified compilation of functional languages.

I expect to be on the academic job market in fall 2021.

I am a contributor in the CertiCoq project. I occasionally contribute to QuickChick and F*.

My CV can be found here.

News

Talks

Publications

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

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