Statement of Purpose Essay - Cornell

My goal as a researcher is to improve our ability to prevent errors in programs. I would like to pursue a PhD in computer science to continue making progress towards this objective. The approach I have focused on in my research is providing static guarantees for programs by 1) describing programs through type systems, and 2) formally proving properties about these programs. In the rest of this statement, I share the experiences that have shaped my approach as well as directed my interests towards programming language (PL) theory, type theory, and proof assistants. Normalization by Evaluation (Spring 2023) Dependently typed programming languages, such as Agda, allow us to define types that depend on programs. I first became interested in them because they provide more static guarantees for programs; they can also be used to write proofs. To learn how to use Agda as a proof assistant, I worked through "Programming Languages Foundations in Agda" in my personal time. The textbook is written in Agda with the hope of being more accessible to students. This inspired me to write an online tutorial with Agda on normalization-by-evaluation (NbE), an algorithm that can be used to implement a type checker for a language with dependent types. In the tutorial, I show how to implement NbE and prove the correctness of the algorithm. The tutorial was adapted from Andreas Abel’s habilitation thesis, which I studied in depth as part of a PhD-level course. Proving the correctness of NbE introduced me to logical relations, a topic I continued to research with Prof. Stephanie Weirich. Making Logical Relations More Relatable (Summer 2023) Logical relations are a versatile tool for proving properties about programs, such as the static guarantee that a well-typed program is terminating. Although the use of proof assistants to teach topics in PL has become increasingly common, there are not enough mechanized tutorials on logical relations. Prof. Weirich and I conjecture this is because proofs by logical relations are known to be especially tedious to mechanize in a proof assistant. In a mechanization, the many additional lemmas required can easily obscure the technique. Although several tools have been developed to aid PL researchers in mechanizing proofs by logical relations, these are aimed towards researchers already familiar with the technique. This motivated us to develop a proof that can be used to introduce logical relations in a mechanized setting. We show that if a term in the lambda calculus can be assigned a type, its evaluation is well-defined. This is a well-known result; what is notable about our proof is that it avoids reasoning about substitutions. Substitution lemmas are often the most tedious part of mechanizing a proof by logical relations. Without substitution lemmas, our proof can be mechanized while keeping logical relations as the main emphasis. I was the first author of a paper we wrote presenting the proof in Agda. It serves as a mechanized tutorial on logical relations; we plan to submit it to ICFP 2024 as a functional pearl. In the future, I would like to continue studying logical relations and their applications in proving static guarantees for programs. I worked on one example of such a proof for an extension to call-by-push-value (CBPV). Effects and Coeffects in Call-By-Push-Value (Fall 2023) CBPV is a computational model that is useful for describing the behavior of programs with effects (e.g. printing). Prof. Weirich, myself, and collaborators observe that CBPV is also appropriate for studying coeffects, the demands a program makes on its environment (e.g. resource usage). Coeffects are dual to effects, so the same should be true for their interaction with CBPV. This is the main theme of a paper we wrote studying the duality of effects and coeffects in CBPV, submitted to OOPSLA 2024 for review. The paper includes a type-and-effect system for CBPV that statically tracks the effects of a computation, along with an operational semantics instrumented with effects. Among our results are effect soundness: the effects of a program at runtime are accurately bounded by our type-and-effect system. Our effects system helps motivate our approach to coeffects and we present parallel results for a coeffects system. My main contribution was to the effects portion of the paper. In addition, I mechanized in Agda all of the results for our effect system. Cornell I would like to work with the PL @ Cornell group, including Prof. Justin Hsu. Prof. Hsu has recently worked on a draft publication on shared and separate effects, which I find motivating as I have studied shared and separate resources from the perspective of CBPV with coeffects. I would be interested in developing a broader theory of separation for effects with Prof. Hsu. I would also like to study how we can use type systems to develop safer network applications with Prof. Nate Foster. I became interested in this area while Prof. Weirich and I collaborated with Prof. David Walker on DeFINE, a functional programming language for the network data plane. I designed a type system for DeFINE and formalized DeFINE’s type system and an operational semantics in Agda. I am also interested in working with Prof. Adrian Sampson, who has recently used a type system to model pipelining constraints on a project featuring a real, working system. I would like to contribute to this project because of my background in software engineering as well as my interest in type systems. Teaching and Career Goals For most of my time as an undergraduate, I was a teaching assistant for an introductory course in computer science. Through this experience, I developed a passion for teaching. As a graduate student, I have continued to teach students and have written tutorials with the hope of explaining difficult topics in PL research to others. As a PhD student, I want to continue teaching and I am especially interested in advising undergraduates in research projects. After completing a PhD, I would like to be a professor at a research university. I will continue my research while mentoring students and fostering their growth.