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.
I am currently working on 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),
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:
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 2021 Type Stability in Julia: Avoiding Performance Pathologies in JIT Compilation
As a scientific programming language, Julia strives for performance but also provides high-level productivity features. To avoid performance pathologies, Julia users are expected to adhere to a coding discipline that enables so-called type stability. Informally, a function is type stable if the type of the output depends only on the types of the inputs, not their values. This paper provides a formal definition of type stability as well as a stronger property of type groundedness, shows that groundedness enables compiler optimizations, and proves the compiler correct. We also perform a corpus analysis to uncover how these type-related properties manifest in practice.
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
FTfJP 2019 Decidable Tag-Based Semantic Subtyping for Nominal Types, Tuples, and Unions
Semantic subtyping enables simple, set-theoretical reasoning about types by interpreting a type as the set of its values. Previously, semantic subtyping has been studied primarily in the context of statically typed languages with structural typing. In this paper, we explore the applicability of semantic subtyping in the context of a dynamic language with nominal types. Instead of static type checking, dynamic languages rely on run-time checking of type tags associated with values, so we propose using the tags for semantic subtyping. We base our work on a fragment of the Julia language and present tag-based semantic subtyping for nominal types, tuples, and unions, where types are interpreted set-theoretically as sets of type tags. The proposed subtyping relation is shown to be decidable, and a corresponding analytic definition is provided. The implications of using semantic subtyping for multiple dispatch are also discussed.
[ Talk ]
Семинар ЯПиК 2019 Семантическое подтипирование на основе типовых тегов (Tag-based Semantic Subtyping)
Venue: Семинар «Языки программирования и компиляторы», Мехмат ЮФУ. Ростов-на-Дону, Россия (Seminar on Programming Languages and Compilers, Rostov-on-Don, Russia) Date: 15 мая 2019 (May 15)
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.
I am currently working on formalizing aspects of
the Julia language.
