People of Programming Languages

An interview project in conjunction with POPL 2018  

 

JY: Tell us about yourself.

ZP: I grew up in Athens, Greece, where I did my undergrad in electrical and computer engineering. I did not know that I wanted to focus on computer science, and in particular programming languages, until the second or third year of my studies. My PL journey started the last year of my studies when I moved to Paris to do an internship with Cătălin Hriţcu for my undergrad thesis. I decided to stay there for my Master’s degree and then I moved to Saarbrucken, Germany, for another internship at Max Planck Institute for Software Systems with Deepak Garg, to complete my Master’s thesis. I currently live in Princeton, New Jersey, doing my PhD with Andrew Appel.

JY: How did you get interested in programming language research?

ZP: During my studies in Greece I took a compilers course. The year I took the course the project was to build a compiler of an OCaml-like language. I very soon realized that this is what I wanted to do! I was very inspired by the elegance of functional languages, the formal foundations, and the connections to logic. After that, I took all the relevant courses offered in my university and started looking for research opportunities.

JY: What are you working on these days?

ZP: My current work is in the context of CertiCoq, a verified compiler for the Coq interactive theorem prover that aims to bridge the gap between certified functional programs and their translation to machine language. I am working on extending the correctness properties beyond functional correctness and prove properties such as absence of memory leaks. This is more challenging as one has to explicitly reason about heap allocation, sharing, and garbage collection but also essential because to claim that a compiler is correct we have to go beyond the correctness of the final result. In parallel, I have started exploring the possible connection of C and Gallina both at the execution and specification level, using CertiCoq and VST.

On the side, I’m working on QuickChick, a property-based testing framework for Coq. QuickChick aims at disproving false propositions by testing. One of the main challenges is that, in Coq, not all propositions are executable and hence amenable to testing. Generating “good” test data is also non trivial, especially in a dependently typed setting, as they often have to satisfy complex invariants. Our work aims at narrowing the gap between testing and proving and making it easier to switch between the two. My friend and collaborator Leo Lampropoulos and I have several exciting ideas for extending our framework that we would like to explore in the future.

JY: How did you get interested in doing research on Coq?

ZP: I was encouraged to learn Coq by Cătălin Hriţcu when we were discussing potential internship topics. I was always concerned with mathematical rigor so the idea of mechanized proofs really clicked with me. I soon started believing that machine-checked proofs should replace pen-and-paper proofs. But for it to become possible and worthwhile we need to lower the cost of mechanization and strengthen the provided guarantees. QuickChick is aimed at the former whereas CertiCoq targets the latter.

Last summer I was an intern at Microsoft Research Redmond working with Nikhil Swamy and Jonathan Protzenko, and so I had the opportunity to work on a different proof assistant, F*. It was very interesting to see the directions the F* team is taking to tackle the above problems and also work in one of them, in particular optimizing tactic execution.

JY: Are there papers or talks that you found particularly inspiring in terms of getting you into programming languages research or your current research?

ZP: Thankfully, there is a lot of inspiring work in the PL community! The most influential line of work for me so far is the one of Amal Ahmed on logical relations. Somehow it keeps coming up in almost every research project I was involved (except maybe QuickChick) and it has helped me make progress numerous times. When I did my master’s thesis with Deepak Garg her early work on step-indexed logical relations was essential for my understanding of these notions. After that, when I started working on CertiCoq, I came across Amal's work again when I was trying to specify the correctness of compiler transformations and understand the compositionality problems. Even last summer, when I was working with Nikhil Swamy and Jonathan Protzenko on formalizing a framework for efficient tactic execution that involved interoperating between F* and OCaml execution, we found out that there were really strong connections between what we were doing and Amal’s work.

JY: Tell us about your undergrad thesis work with Cătălin.

ZP: With Cătălin I worked on QuichChick. Our work extended QuickChick with a verification framework that allowed to specify and prove correct random data generators, and ultimately prove that the testing code checks the desired logical proposition. More precisely, the framework allows to prove a generator sound and complete with respect to a set, meaning that all the elements that can be generated are in that set and all the elements of the set can be potentially generated. Such sets can be as simple as the set of natural numbers, or more complex ones such as the set of balanced search trees or the set of well-typed terms for a notion of well-typedness. The idea came by realizing that once we had a testing framework build inside a proof assistant we might as well try to prove things about it!

JY: Tell us about the paper you have that's upcoming in this next POPL. What's it about and how did it come about?

ZP: The paper is about automatically generating efficient random generators in QuickChick that satisfy invariants in the form of inductive relations, and also proofs certifying that the generators are sound and complete with respect to this relation. For QuickChick users that means that they can derive complex random data generators for free along with their correctness proofs! This idea felt like a natural next step for QuickChick. One day Leo Lampropoulos asked me “If I automatically generate generators can you automatically generate their proofs of correctness?”. The rest is in the POPL paper!

JY: What problems are you most excited to see the community solve in the next five to ten years?

ZP: The community is making a lot of exciting progress in making verification tractable and applicable to real-world situations. One aspect of this that I'm thinking about these days is how we could make verification of multi-language programs feasible and create verification environments that allow the specification and the verification of foreign function interfaces. That raises many interesting problems, like being able to interface different program logics, that I would like to see being solved in the next few years.