Ezgi Çiçek is a final year PhD student at Max Planck Institute for Software Systems (MPI-SWS) and Saarland University under the supervision of Deepak Garg. For her thesis work, she developed type-theoretic techniques for relational cost analysis. We talk about her path to getting integrated in the POPL community, how she came to do her thesis work on relational cost analysis, and how she plans to apply this work to real code next.
JY: Tell us about yourself.
EC: I am originally from Bursa, Turkey. I went to a boarding high school where we had limited access to computers but great exposure to math and geometry. For an independent high school project, I went to the local university and learned about algorithms. I was intrigued by the topic and that's how I decided to study computer science. For my undergrad, I went to Bilkent University in the Turkish capital, Ankara. While in Bilkent, I had several opportunities to expand my horizons and try out various things: I did a research internship at University College Dublin in Ireland, participated in Google Summer of Code, spend a year abroad at the University of California, San Diego as an exchange student, and interned at Sony's Testing and Debugging team in San Diego.
Right after finishing my undergrad in Bilkent, I joined MPI-SWS in Germany to do a PhD in Programming Languages with Umut Acar on incremental computation, about analyzing software to only rerun the necessary parts of a program when inputs change. Umut moved to CMU one year after I joined and that's how I started to work with my current advisor, Deepak Garg. Back then, Deepak was mainly interested in foundations of computer security and privacy, but he was generous enough to advise me on cost analysis of incremental computations, a somewhat unrelated topic to his background, about analyzing programs for how much it costs to rerun them when inputs change. It has been a great pleasure working with Deepak and in the end, it all worked out—I have recently submitted my thesis and can't wait to officially graduate!
JY: How did you get interested in programming language research?
EC: During my exchange year at UCSD, I took courses on compilers and programming languages and also did a mini research project on query languages. I really enjoyed these courses and wanted to learn more about programming language techniques. That's how I got the idea to do a PhD in programming languages.
JY: Are there papers or talks that you found particularly inspiring in terms of getting you into programming languages research or your current research?
EC: When I first read a type theory paper during my first year in grad school, I had a very difficult time understanding all the Greek symbols and terminology. As time passed, I started to acquire more knowledge and along with it came more understanding. Attending summer schools like Oregon Programming Languages Summer School (OPLSS) and Midlands Graduate School (MGS) were also very inspiring.
In my second year in grad school, I took Derek Dreyer's course on logical relations at MPI-SWS. At the time, the technique seemed very useful but the whole thing was quite abstract to me. It all made sense when I had a chance to apply it directly in my research and extend logical relations with relational effects.
I was also inspired by Pfenning and Xi's work on DML and Gaboardi et al.'s DFuzz. Both DML and Dfuzz enrich the underlying type system with lightweight dependent types in order to verify interesting properties such as memory safety and differential privacy. They struck a nice balance between expressivity and practicality of typechecking. In my thesis work, I aspired to have this balance when designing a refinement type system for relational cost analysis.
JY: Tell us about your thesis work and your POPL'17 paper. What are they about and how did they come about?
EC: My thesis work originated from our early work on cost analysis of incremental computation. The idea behind incremental computation is that whenever a piece of data changes, the underlying runtime system attempts to save time by only recomputing those parts of the program that depend on the changed data. This ability to partially evaluate makes incremental computation potentially very efficient. For instance, incremental runs of many applications, such as spreadsheet computations, build processes and web-crawling, can be asymptotically much more efficient than their from-scratch runs. While incremental computation makes efficient design possible in many cases, for schedulability and resource allocation, it is often important to establish how much of a speedup one could gain from incremental computation. Moreover, such an analysis often depends on many factors such as input changes, execution traces, which can be viewed as graphs of computations and their (run-time) data and control dependencies. Motivated by the lack of high-level static analyses for reasoning about computational complexity of incremental programs, we developed DuCostIt, a refinement type and effect system for verifying update times of incremental programs, which was published in ICFP'16.
Later on, we realized that we could adapt this type-based verification technique to reason about not only incremental computational complexity for the same program, but also relative cost—in terms of complexity and also other resource usage metrics—of two different, possibly similar, programs. Relational cost analysis can be useful in many different settings. In resource-aware compiler verification, we can prove that optimized code runs at least as fast as the original code. In side-channel analysis for security, we can prove that resource consumption does not leak any confidential information. In approximate computation, we can prove that an approximate algorithm achieves the desired level of efficiency. Our POPL 2017 paper is about RelCost, a refinement type system that enables such a relational cost analysis in a higher-order functional language with recursion and subtyping. The key novelty of RelCost is the combination of relational refinements with two modes of typing—relational typing for reasoning about similar computations/inputs and unary typing for reasoning about unrelated computations/inputs. This combination allows us to analyze the execution cost difference of two programs more precisely and locally than a non-relational approach. In my thesis, I also designed an algorithmic type-checking mechanism and implemented a prototype for RelCost.
I think it’s really exciting that type systems allow us to do this potentially very useful relational analysis before a program even runs. My thesis makes some good steps towards making this possible.
JY: What are you working on these days?
EC: As of January, I am going to be joining Static Analysis team at Facebook in London as a Research Scientist and Software Engineer. I hope to work on adapting my thesis work on relational cost analysis to millions of lines of imperative code. What makes relational cost analysis attractive to big code bases is its potential to be scalable and diff-based: for many cases it suffices to just analyze the code diff to figure out if programmers introduce any performance bugs. This allows relational cost analysis can be used to analyze an evolving code base much more efficiently and scalably compared to a non-relational global analysis.
JY: Do you have stories to share from your experiences attending POPL?
EC: I have attended POPL four times, thanks to the generous funding by MPI-SWS and also the mentoring workshop, PLMW. Initially, I found the community very hard to get into: I didn't have much background to understand most of the talks and didn't know how to start conversations. Attending PLMW was great for getting over my initial newbie fears.
There is an anecdote I can share: a professor who has seen me over the years at PL conferences used to asked me if I have finally a paper at POPL. His remarks were not comforting but they were also good fuel for my first POPL paper. I encourage grad students to take the opportunity and go to POPL or other PL conferences and not to be demotivated ;). At least, you get to meet with other researchers and potential collaborators.
JY: What do you like most about the POPL community?
EC: From a technical perspective, I like the principled and rigorous approach the community takes on solving problems and evaluating work. I submitted to POPL several times and the reviews have been very thoughtful and high quality. From a community perspective, I will mention two things. First, the mentoring workshop, PLMW, has been beneficial in my career to develop as a PL researcher. Second, I appreciate the events held to commemorate passing scientists such as John Reynolds and Kohei Honda. I like reading obituaries and such events remind me that those influential researchers who contributed to programming languages were also human and full of interesting stories.