Home

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. Recently, I have been working on program analysis techniques for combining over- and under-approximate reasoning in the context of symbolic execution. My thesis 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.

Contacts

Email: julbinb@gmail.com (preferred) or ybelyako@purdue.edu
Professional: github, researchgate, linkedin
Social: twitter, facebook
Current location (as of 2024): Lafayette, IN, USA
Office: 3154C, Lawson Computer Science Building
Book a meeting: calendly

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.

Short bio (full bio, personal)

I was born in 1991 in Russia, Rostov-on-Don, where I also grew up and received education. In 2012–2016, I was teaching undergraduate CS courses at my alma mater, Faculty of Mathematics, Mechanics and Computer Science (Southern Federal University).
While teaching half-time, I had entered a PhD program as well but later moved to Northeastern where my PhD journey started over.
In 2017–2018, I spent a year at the Faculty of Information Technology (Czech Technical University in Prague) doing research with Jan Vitek.
In 2018–2023, I continued working with Jan Vitek during my PhD at Khoury College of Computer Sciences (Northeastern University) in Boston.
In 2023, I started a postdoc with Suresh Jagannathan at PurPL (Purdue University).

Recent professional news (without failures)

Nov 2024: accepted paper at POPL 2025
Derivative-Guided Symbolic Execution
Aug 2024: joined the Review Committee of OOPSLA 2025
Apr 2024: accepted paper at PLDI 2024
Decidable Subtyping of Existential Types for Julia
Apr 2024: joined the Program Committee of Scheme 2024
Feb 2024: joined the Program Committee of TyDE 2024
Jan 2024: joined the Program Committee of ARRAY 2024
Nov 2023: talk at PurPL Seminar
Julia: Practical Restrictions for a Scientific-Computing Language
Aug 2023: defended my PhD thesis at Northeastern University
Decidable Subtyping of Existential Types for the Julia Language

Research

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, program analysis, 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.

Most recently, I have been working on program analysis, in particular, on extending symbolic execution with symbolic finite automata (POPL 2025) and enabling symbolic execution to reason about over-approximate information (work in progress).

During my PhD, I worked on formalizing various aspects of the Julia programming language:

The notion of type stability and its impact on JIT compilation in Jules [OOPSLA 2021].
The semantics of world age and its interaction with eval in a core calculus Juliette [OOPSLA 2020].
The subtyping relation.
- A reconstruction of subtyping in LambdaJulia [OOPSLA 2018].
- A semantic subtyping model suitable for a dynamic programming language [FTfJP 2019, Appendix A.2 of PhD thesis].
- Decidable subtyping [PhD thesis] [PLDI 2024]

Disclaimer. Good or bad, the language has nothing to do with me, and our shared name is a coincidence!

My previous research was related to language support for generic programming in object-oriented languages [SBLP 2016, SYRCoSE 2015].

Selected papers and talks

PLDI 2024
Decidable Subtyping of Existential Types for Julia
Authors: Julia Belyakova, Benjamin Chung, Ross Tate, Jan Vitek
DOI: 10.1145/3656421
Venue: Proc. ACM Program. Lang., Volume 8, PLDI, Article 191 (24 pages)
Reviews

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
Venue: Principles of Programming and Verification Seminar (Boston University). Boston, MA, USA. Online
Date: Oct 12, 2021

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
Authors: Julia Belyakova, Benjamin Chung, Jack Gelinas, Jameson Nash, Ross Tate, Jan Vitek
DOI: 10.1145/3428275
Venue: Proc. ACM Program. Lang., Volume 4, OOPSLA, Article 207 (26 pages)
Reviews

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.
VIS 2020 (short paper)
Just TYPEical: Visualizing Common Function Type Signatures in R
Authors: Cameron Moy, Julia Belyakova, Alexi Turcotte, Sara Di Bartolomeo, Cody Dunne
DOI: 10.31219/osf.io/pyqac
Venue: IEEE Visualization Conference 2020, Short Papers, OSF Preprints (5 pages)

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
Authors: Francesco Zappa Nardelli, Julia Belyakova, Artem Pelenitsyn, Benjamin Chung, Jeff Bezanson, Jan Vitek
DOI: 10.1145/3276483
Venue: Proc. ACM Program. Lang., Volume 2, OOPSLA, Article 113 (28 pages)

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
Authors: Julia Belyakova
DOI: 10.1007/978-3-319-45279-1_1
Venue: LNCS Programming Languages: 20th Brazilian Symposium on Programming Languages, Volume 9889, Article 1 (15 pages)

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.