We consider the formulation of a symbolic execution (SE) procedure for functional programs that interact with effectful, opaque libraries. Our procedure allows specifications of libraries and abstract data type (ADT) methods that are expressed in Linear Temporal Logic over Finite Traces (LTLf), interpreting them as symbolic finite automata (SFAs) to enable intelligent specification-guided path exploration in this setting. We apply our technique to facilitate the falsification of complex data structure safety properties in terms of effectful operations made by ADT methods on underlying opaque representation type(s). Specifications naturally characterize admissible traces of temporally-ordered events that ADT methods (and the library methods they depend upon) are allowed to perform. We show how to use these specifications to construct feasible symbolic input states for the corresponding methods, as well as how to encode safety properties in terms of this formalism. More importantly, we incorporate the notion of symbolic derivatives, a mechanism that allows the SE procedure to intelligently underapproximate the set of precondition states it needs to explore, based on the automata structures implicit in the provided specifications and the safety property that is to be falsified. Intuitively, derivatives enable symbolic execution to exploit temporal constraints defined by trace-based specifications to quickly prune unproductive paths and discover feasible error states. Experimental results on a wide-range of challenging ADT implementations demonstrate the effectiveness of our approach.
PLDI 2024🔗 Decidable Subtyping of Existential Types for Julia
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.
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 2021 Extended (arXiv)🔗 Type Stability in Julia: Avoiding Performance Pathologies in JIT Compilation (Extended Version)
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.
OOPSLA 2020 Extended (arXiv)🔗 World Age in Julia: Optimizing Method Dispatch in the Presence of Eval (Extended Version)
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.
SYRCoSE 2016🔗 Language Support for Generic Programming in Object-Oriented Languages: Design Challenges
It is generally considered that object-oriented (OO) languages provide weaker support for generic programming (GP) as compared with functional languages such as Haskell or SML. There were several comparative studies which showed this. 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 the earlier comparative studies object-oriented languages were usually not treated in any special way. However, the OO features affect language facilities for GP and a style people write generic programs in such languages. In this paper we compare ten modern object-oriented languages and language extensions with respect to their support for generic programming. It has been discovered that every of these languages strictly follows one of the two approaches to constraining type parameters. So the first design challenge we consider is “which approach is better”. It turns out that most of the explored OO languages use the less powerful one. The second thing that has a big impact on the expressive power of a programming language is language support for multiple models. We discuss pros and cons of this feature and its relation to other language facilities for generic programming.
SYRCoSE 2015🔗 Pitfalls of C# Generics and Their Solution Using Concepts
As was shown in earlier studies, in comparison with Haskell type classes and C++ concepts such mainstream object-oriented languages as C# and Java provide much limited mechanisms of generic programming based on F-bounded polymorphism. Main pitfalls of C# generics are carefully considered in this paper. A special attention is given to drawbacks of recursive constraints (F-constraints), ambiguous semantics of interfaces, lack of language support for multi-type constraints and retroactive interface implementation, and subtle problems of the Concept design pattern, which is widely used not only in C#, but in Java and Scala as well. To solve the problems of C# generics, extending C# language with concepts is proposed: as a new language construct, concepts are to be used as constraints on type parameters exclusively, with object-oriented interfaces being used as types. In contrast to basic C++ concepts, C# concepts may include subtype and supertype constraints, allow constraints aliasing and automatic generation of default models. The major differ-ence of the concepts design proposed is language support for multiple models. The latter feature is supported neither in C++ concepts, nor in Haskell type classes. In conclusion, a mechanism of implementation of concepts via translation to basic C# is outlined. The most important property of the translation is a possibility to recover a source code in extended language from a compiled module.
Workshops
TPSA 2025🔗 From Traces to Program Incorrectness: A Type-Theoretic Approach
We present a type-theoretic framework for reasoning about incorrectness in functional programs that interact with effectful, opaque library APIs. Our approach centers on traces – temporally-ordered sequences of library API invocations – which naturally characterize both the preconditions of individual APIs and their composite behavior. We represent these traces using symbolic regular expressions (SREs), enabling formal specification of incorrect abstract data type (ADT) behaviors across function boundaries. The core contribution is a novel type inference algorithm that operates modulo specified incorrectness properties and leverages the symbolic finite automata (SFAs) representations of regexes for compositional reasoning of traces. When the algorithm succeeds, the inferred types witness that an ADT implementation can exhibit some subset of the specified incorrect behaviors. This represents the first systematic approach to underapproximate reasoning against trace-based incorrectness specifications, enabling a new form of trace-guided compositional analysis.
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.
FTfJP 2017🔗 Generic Approach to Certified Static Checking of Module-like Constructs
Extended Abstract Authors:Julia Belyakova DOI:10.1145/3103111.3104045 Venue: Proc. 19th Workshop on Formal Techniques for Java-like Programs, Article 5 (2 pages)
In this paper we consider the problem of certified static checking of module-like constructs of programming languages. We argue that there are algorithms and properties related to modules that can be defined and proven in abstract way. We advocate the design of a generic Coq library, which is aimed to provide three building blocks for each checking mechanism: propositional, computable, and correctness proofs. Implemented part of the library is justified by applying it to a certified static checker of an extension of STLC.
Authors:Julia Belyakova Venue: Northeastern University ProQuest Dissertations Publishing, 2023
Julia is a dynamic, high-performance programming language for scientific computing. To encourage a high level of code reuse and extensibility, Julia is designed around symmetric multiple dynamic dispatch, which allows functions to have multiple implementations tailored to different argument types. To resolve multiple dispatch, Julia relies on a subtype relation over a complex language of run-time types and type annotations, which include set-theoretic unions, distributive tuples, parametric invariant types, and impredicative existential types. Notably, subtyping in Julia is undecidable, which manifests with a run-time stack-overflow error when program execution encounters a subtyping query that causes the subtype checker to loop. In this dissertation, I propose a decidable subtype relation for a restricted language of Julia types where existential types inside invariant constructors are limited to ones expressible with use-site variance. To estimate the migration effort that would be required for switching to the restricted type language, I analyze type annotations in the corpus of 9K registered Julia packages. Out of 2M statically identifiable type annotations in the corpus, 99.99% satisfy the restriction, making it a viable candidate for evolving Julia towards decidable subtyping.
Публикации (Publications in Russian)
TBD
Журналы списка ВАК
Современные ИТ 2015 Концепт-параметры как механизм развития средств обобщённого программирования в языке C# (Concept Parameters as a Mechanism of Development of the Language Support for Generic Programming in C#)
Authors:Ю. В. Белякова,
С. С. Михалкович Venue: Научный журнал «Современные информационные технологии и ИТ-образование», том 2 (№ 11)
Дистанционное обучение 2012 Использование веб-среды PascalABC.NET для дистанционного обучения программированию (Using a Web-Environment PascalABC.NET for Distance Teaching of Programming)
В работе описывается интегрированная веб-среда программирования PascalABC.NET WDE. Основное внимание уделяется особенностям среды и связанным с ней сервисам, которые позволяют эффективно использовать ее при организации дистанционного обучения. (An integrated web-environment PascalABC.NET WDE is described in the article. Great attention is paid to its features and related services that enable to use it effectively in organizing distance education.)
Сборники конференций
Ю. В. Белякова.
Реализация сертифицированного интерпретатора для расширения
простого типизированного лямбда-исчисления с концепт-параметрами //
Труды конференции памяти А.Л. Фуксмана
«Языки программирования и компиляторы 2017».
Ростов-на-Дону, 3–5 апреля 2017 — С. 53−58 (TODO: links)
…
Образование
Магистерская диссертация
«Модель концептов в императивном языке программирования» (2014 г.)
Реферат «Алан Тьюринг» (2013 г.) (TODO: link)
Сообщение «Никлаус Вирт и его языки программирования»
(2013 г.) (TODO: link)
Выпускная квалификационная работа бакалавра
«Автоматическое построение ограничений в модельном языке программирования
с шаблонами функций и автовыводом типов» (2012 г.)
Курсовая работа
«Модельный язык программирования с λ-функциями» (2011 г.)
