I am 4th year PhD student in the University of Pennsylvania advised by Sebastian Angel and Steve Zdancewic. My interests include the reliability, security and privacy of computer systems, both through program verification (Coq, Z3, F*) and cryptographic zero-knowledge proofs (zkSNARKs), I believe the two approaches are complementary. I will be looking for research scientist jobs starting in 2025, feel free to reach out.
-
About Me
Interests
Bio
Before starting my PhD I worked for 5 years in industry as a Software Engineer (Bridgewater Associates, Apple) and Tech Lead at UnifyID. I completed by Bachelor’s and Masters in MIT my thesis advisors were Frans Kaashoek and Nickolai Zeldovich. I am from Thessaloniki, Greece and I like hiking, snowboarding and camping.
-
posts
-
Formalizing Permutation Networks
Confidential communication is not only important, but necessary in plenty of scenarios, from online purchases to communicating military intelligence. In order to achieve trust and confidentiality in communications computer scientists invented cryptographic protocols. While the theory behind cryptographic protocols has been rigorously formalized, their implementations are not and prone to bugs. This space is fertile grounds for formal verification of computer programs, which has had success in both academia and industry[1][2].
-
Algebraic datatypes in C++17
In functional languages, algebraic types are an important part of the user experience and the most complete and minimal way to define data structures. In the Coq proof assistant, the polymorphic list definition is inductively defined, here is what it looks like.