I am a postdoc at Purdue University (West Lafayette, IN, USA).
I work with Suresh Jagannathan
at PurPL, the Purdue University Programming Language Group,
starting September 2023.
My research focuses on programming languages, in particular,
their design, semantics, and correctness.
My most recent work was about formalizing aspects of
the Julia language.
🇺🇦 As a Russian national, I strongly condemn the war started by the Russian government in Ukraine on February 24th, 2022.
If you have any questions or comments—about projects, papers,
or anything else mentioned on the website
(e.g. international student experience, being a woman
in CS)—please, feel free to email me or submit your feedback using this Google form. I would be happy to answer questions that you might have, learn about what is unclear or confusing, or receive any other feedback.
My research largely focuses on the design, semantics, and correctness
of programming languages.
In particular, I am interested in making it easier for language users
to understand the semantics of their programming language
and write robust and correct software.
My research interests also include type systems, compilers,
software correctness, theorem proving (most of my experience has been with
The Coq Proof Assistant),
generic programming (like Java generics or ML polymorphism),
programming by contracts, software testing,
human aspects of programming languages and software engineering,
and CS education.
For the last several years I have been working on formalizing
various aspects of the Julia
programming language:
Julia is a modern scientific-computing language that relies on multiple dispatch to implement generic libraries. While the language does not have a static type system, method declarations are decorated with expressive type annotations to determine when they are applicable. To find applicable methods, the implementation uses subtyping at run-time. We show that Julia’s subtyping is undecidable, and we propose a restriction on types to recover decidability by stratifying types into method signatures over value types—where the former can freely use bounded existential types but the latter are restricted to use-site variance. A corpus analysis suggests that nearly all Julia programs written in practice already conform to this restriction.
[ Talk ]
PurPL 2023 Julia: Practical Restrictions for a Scientific-Computing Language
Venue:PurPL Seminar (Purdue University). West Lafayette, IN, USA Date: Nov 30, 2023
Julia is a high-level, dynamic programming language for scientific computing. To achieve performance, Julia relies on an optimizing just-in-time compiler. To make compilation predictable and allow for a simpler compiler implementation, the language is intentionally designed around a few unusual restrictions. In the first part of the talk, we discuss “world age”—the semantics of eval function for dynamically executing code. Unlike other dynamic languages, Julia delays when eval’ed code becomes available to the rest of the program, thus allowing the compiler to retain pre-eval optimizations. A corpus analysis of Julia code shows that such delaying semantics is practical in most cases. In the second part of the talk, we discuss a restriction on Julia’s type language that would allow for decidable subtyping. Julia’s dynamic dispatch is currently resolved with undecidable subtyping, meaning that in practice, a program can crash with a stack-overflow error due to an unfortunate subtype query. The decidability of subtyping can be recovered by restricting existential types inside invariant type constructors to use-site variance. A corpus analysis of Julia code shows that the vast majority of existing programs already adhere to this restriction.
[ Talk ]
POPV 2021 Julia: Language Design and Users Working Together
As a programming language for scientific computing, Julia strives for predictable performance as well as flexibility and ease of use. To tackle this challenge, Julia employs two strategies. First, it enables highly compositional programs by using multiple dispatch as the core paradigm, but at the same time, pragmatically restricts the language to facilitate optimizations. Second, Julia enables productive collaboration between the programmer and the JIT compiler by making the compiler’s behavior predictable and encouraging optimization-conducive coding discipline. In this talk, we look at several components of this two-fold approach. We start with an overview of multiple dispatch. Next, we talk about type stability, a property of the code that enables the key optimization in Julia’s optimization pipeline. Finally, we look at the world age, a mechanism that allows for a pragmatic trade-off between flexibility of “eval” and predictability of compiler optimizations.
OOPSLA 2020 World Age in Julia: Optimizing Method Dispatch in the Presence of Eval
Dynamic programming languages face semantic and performance challenges in the presence of features, such as eval, that can inject new code into a running program. The Julia programming language introduces the novel concept of world age to insulate optimized code from one of the most disruptive side-effects of eval: changes to the definition of an existing function. This paper provides the first formal semantics of world age in a core calculus named Juliette, and shows how world age enables compiler optimizations, such as inlining, in the presence of eval. While Julia also provides programmers with the means to bypass world age, we found that this mechanism is not used extensively: a static analysis of over 4,000 registered Julia packages shows that only 4-9% of packages bypass world age. This suggests that Julia's semantics aligns with programmer expectations.
Data-driven approaches to programming language design are uncommon. Despite the availability of large code repositories, distilling semantically-rich information from programs remains difficult. Important dimensions, like run-time type data, are inscrutable without the appropriate tools. We contribute a task abstraction and interactive visualization, TYPEical, for programming language designers who are exploring and analyzing type information from execution traces. Our approach aids user understanding of function type signatures across many executions. Insights derived from our visualization are aimed at informing language design decisions — specifically of a new gradual type system being developed for the R programming language. A copy of this paper, along with all the supplemental material, is available at osf.io/mc6zt
OOPSLA 2018 Julia Subtyping: A Rational Reconstruction
Programming languages that support multiple dispatch rely on an expressive notion of subtyping to specify method applicability. In these languages, type annotations on method declarations are used to select, out of a potentially large set of methods, the one that is most appropriate for a particular tuple of arguments. Julia is a language for scientific computing built around multiple dispatch and an expressive subtyping relation. This paper provides the first formal definition of Julia's subtype relation and motivates its design. We validate our specification empirically with an implementation of our definition that we compare against the existing Julia implementation on a collection of real-world programs. Our subtype implementation differs on 122 subtype tests out of 6014476. The first 120 differences are due to a bug in Julia that was fixed once reported; the remaining 2 are under discussion.
SBLP 2016 Language Support for Generic Programming in Object-Oriented Languages: Peculiarities, Drawbacks, Ways of Improvement
Earlier comparative studies of language support for generic programming (GP) have shown that mainstream object-oriented (OO) languages such as C# and Java provide weaker support for GP as compared with functional languages such as Haskell or SML. But many new object-oriented languages have appeared in recent years. Have they improved the support for generic programming? And if not, is there a reason why OO languages yield to functional ones in this respect? In this paper we analyse language constructs for GP in seven modern object-oriented languages. We demonstrate that all of these languages follow the same approach to constraining type parameters, which has a number of inevitable problems. However, those problems are successfully lifted with the use of the another approach. Several language extensions that adopt this approach and allow to improve GP in OO languages are considered. We analyse the dependencies between different language features, discuss the features' support using both approaches, and propose which approach is more expressive.
I am a postdoc at Purdue University (West Lafayette, IN, USA).
I work with Suresh Jagannathan
at PurPL, the Purdue University Programming Language Group,
starting September 2023.
My research focuses on programming languages, in particular,
their design, semantics, and correctness.
My most recent work was about formalizing aspects of
the Julia language.
