Since its foundation in 2012 by Dmitri Boulytchev, the laboratory has been carrying out scientific research in the area of programming language theory, with the main focus on the following topics:
The other important focus of the laboratory is education. The laboratory, which is open to both undergraduates and graduate students, gets students involved in research projects and provides an opportunity to join related PhD programs. Also, the laboratory members have been designing, lecturing, and assisting courses on the following themes:
Additionally, the laboratory carries out the following activities:
New members are always welcome at the laboratory. The best way to join the group is to attend either our weekly seminar or our open courses and then choose one of the available research topics to pursue.
miniKanren is a family of small embedded languages that bring the power of relational (pure logic) programming to general-purpose programming.
The IMM framework simplifies proving correctness of compilation from programming language memory models, like Promising and Weakestmo, to hardware memory models, like x86, Power, Arm, and RISC-V. The framework is mechanized in Coq.
How should an infinite execution be restricted in a weak memory setting? When does a concurrent program terminate in that setting? It is questions like these that our project aims to answer.
Pomsets with Preconditions, PwT, is aimed to provide a denotational memory model for programming languages which solves the Out-Of-Thin-Air problem without sacrificing performance on modern CPUs. This could be used to replace the C++ memory model.
Under this umbrella project, we’re working on model-checking tools that help uncover sophisticated bugs in concurrent programs.
Mechanized theory of various non-interleaving models of concurrent computation in the Coq Proof Assistant.
This project aims to bring new features to ML-like languages and produce patches fixing ad-hoc or poorly designed language features, such as polymorphic variants, active patterns, and modules.
The aim of this project is to research and practically apply metacomputation techniques, such as partial evaluation, supercompilation, and distillation.
The aim of this project is to develop and practically apply semi-local LCS and SA algorithms.
The lab seminars take place every week and they are open to everyone. We talk about classic and recent research results of programming languages and language tools in the seminars.
A. Jeffrey, J. Riely, M. Batty, S. Cooksey, I. Kaysin, A. Podkopaev
E. Moiseenko, V. Gladstein, A. Podkopaev, D. Koznov
The idea behind the summer/winter school program is to bring together motivated students, post-graduates, and software developers with prominent world-class researchers. One particular topic is studied at each school, which allows the participants to immerse in intensive study and complete an extensive course, which could easily be a semester-long, in just five days. The topics are selected to be on a cutting-edge in the area of programming languages, compilers, development of language tools.