Statement of Purpose Essay - University of Pennsylvania

Statement of Purpose University of Pennsylvania Mayank Keoliya PhD Program in CS mayank@u.nus.edu Motivation. I want to pursue a Ph.D. in Computer Science because I aspire to research programming languages (PL) at an industrial lab. My research interests lie in PL design, program synthesis, and formal methods. My motivation to pursue research stems from my experience working on two research projects in the fields of DNA storage and PL respectively. Through these projects, I have found that I enjoy working on yet-unsolved and challenging problems. I also learnt valuable skills in the ideation, implementation, and communication of research ideas. I’m excited about research in PL because I resonate with its emphasis on finding better program abstractions to solve challenging problems in computer science, such as maintaining verified software. I was introduced to PL through coursework, and grew to appreciate how program abstractions such as continuations and formal specifications can enable greater expressivity and safety. Program synthesis and formal methods aim to improve expressivity and safety by synthesizing implementations and verifying specifications, but are often not able handle complex programs and require significant user expertise. Which begs the question: how can we make the implementation and verification of complex programs more feasible? My past research in formal methods has dealt with subsets of this broad question and highlighted open areas which I aim to tackle. Research in DNA Storage. In Fall 2021, under the supervision of Professor Djordje Jevdjic, I led a project to design a DNA storage simulator. The motivation for the project was to reduce the time and cost of running DNA experiments. I used classic string alignment algorithms to locate the origin of errors, and identified a key simulation parameter: the intra-strand error position of molecules. The addition of this parameter made our simulator 74% more accurate compared to state-of-the-art simulators. No prior work had compared DNA simulators, so I proposed sound evaluation criteria to measure DNA simulator accuracy. My work was later used by Djordje’s group to rapidly evaluate new DNA reconstruction algorithms, and presented as a poster at ISPASS ’22. Research in Programming Languages. In Spring 2022, I took a PL design class with Professor Ilya Sergey. As part of my term project, I implemented a continuation-passing interpreter for a JavaScript dialect which had support for primitive operators for delimited and undelimited continuations. In another class about Coq by Professor Olivier Danvy, I verified a simplified form of the same interpreter, which introduced me to specifications as program abstractions, and deepened my wonder of continuations. This excited me enough to extend my term project by writing a small logic programming language as an abstraction over primitive continuations in JavaScript. Later in summer 2022, I began research on the problem of proof repair with Ilya and PhD student Kiran Gopinathan. The problem was framed as follows: given a library with old and new programs which satisfy the same specification, and a formal proof of correctness for the old version, produce a proof for the new version. The key challenge in building the new proof was invariant inference for higher-order function applications. Over the next six months, we built a tool which reduced invariant inference to a synthesis problem in a two-step process: (i) generating well-typed invariant candidates, and (ii) pruning candidates using tests extracted from function specifications. My primary contribution was step (i), for which I developed a sketch-based technique for enumerative synthesis of well-typed invariant candidates. At the suggestion of my collaborators, I derived the sketches from relevant parts of the old proof, which were in turn obtained by program alignment. Later, I devised separation-logic based heuristics to constrain the space of generated candidates. I implemented these heuristics using a static analysis procedure which filtered irrelevant invariant candidates, such as those which referenced unused heaplets. The sketch-guided synthesis and heuristics together generated few but high-confidence candidates which made the second step of pruning candidates feasible. I conducted an empirical evaluation of our tool by collecting evolved versions of 14 real-world OCaml programs from verified libraries. I verified that our tool quickly produces provably correct invariants for each program and reduces proving time by a factor of 10. While performing the evaluation and browsing several OCaml libraries, I identified a future application of our work in proof migration: the migration of proofs of similar programs from verified to unverified libraries. We have submitted our work to a flagship conference on formal methods. Future Work. During my PhD, I want to enjoy the freedom to work on challenging problems which both advance theoretical understanding and improve developer productivity. I have identified two such problems through my research: building better program abstractions via deductive synthesis, and improving the ease of formal verification. Both problems require providing formal specifications which are often as complicated as the programs they target. To solve this, I want to explore devising simple yet expressive specification-languages for mainstream PLs, which can drastically improve the process of both implementing and proving properties about programs. Outreach. In addition to research, I am passionate about spreading hacker culture and free software. As part of a university club, I organized Singapore’s largest hackathon with 600+ participants, and led over two dozen workshops and talks to introduce beginners to ideas in tech and PL. During my work, I noticed that it is difficult for freshmen, particularly women and international students, to explore extra-curricular activities and navigate a stressful first year since they lacked empathetic and relatable role models. To solve this problem, I started a peer mentorship program to match freshmen with seniors who help them transition to university life. The program has helped over 100 freshmen in two years, and will be scaled to all 800 computing freshmen next year, in partnership with the NUS School of Computing. Faculty. I want to pursue my PhD at Penn because it offers me a collaborative research atmosphere, and its faculty fits well with my research interests. In particular, I am interested in working with Professor Mayur Naik, Professor Osbert Bastani, and Professor Benjamin Pierce. I’m excited by Prof. Naik’s work on Scallop, and its novel probabilistic deductive database approach to neurosymbolic programming. I would like to work on improving the expressivity of Scallop’s Datalog-based declarative language beyond simple recursion and aggregation. Prof. Bastani’s work on ML-enhanced programming via neurosymbolic program synthesis (WebQA) and modular specification-based languages for RL tasks (SPECTRL) fit well with my interests. I’m also interested to work with Prof. Pierce on enhancing property-based testing with QuickChick. With its excellent faculty and resources, Penn is the ideal place for me to embark on my PhD journey.