Researcher in Programming Languages (PL) and Verification (Proof Assistants), soon-to-be using Large Language Models (LLMs) to verify programs in Microsoft Research’s RiSE group.

I completed my PhD in the University of Pennsylvania advised by Sebastian Angel and Steve Zdancewic, where I developed Domain-Specific Programming Languages (DSLs) to improve the reliability, security and privacy of computer systems, combining techniques from formal verification and cryptographic protocols. Before starting my PhD I worked in industry as a Software Engineer (Bridgewater Associates, Apple) and Tech Lead at UnifyID. I completed by Bachelor’s and Masters in MIT and my thesis advisors were Frans Kaashoek and Nickolai Zeldovich. I am from Thessaloniki, Greece and started my academic career at the Aristotle University of Thessaloniki (AUTH).

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].

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.