Programming Languages and Tools Lab
Publications
An Empirical Study of Partial Deduction for MiniKanren
March 2021
Ekaterina Verbitskaia, Daniil Berezun, Dmitry Boulytchev
Beyond the elementary representations of program invariants over algebraic data type
2021
Kostyukov Yurii, Dmitry Mordvinov, and Grigory Fedyukovich
Mechanized Theory of Event Structures: A Case of Parallel Register Machine
2021
Vladimir Gladstein, Dmitrii Mikhailovskii, Evgenii Moiseenko, Anton Trunov
Reimplementing the Wheel: Teaching Compilers with a Small Self-Contained One
2021
Daniil Berezun, Dmitry Boulytchev
Recursive Expressions for SPARQL Property Paths
August 2020
Ciro Medeiros, Umberto Costa, Semyon Grigorev, Martin A. Musicante
Context-Free Path Querying by Kronecker Product
August 2020
Egor Orachev, Ilya Epelbaum, Rustam Azimov, Semyon Grigorev
Context-free path queries (CFPQ) extend the regular path queries (RPQ) by allowing context-free grammars to be used as constraints for paths. Algorithms for CFPQ are actively developed, but J. Kuijpers et al. have recently concluded, that existing algorithms are not performant enough to be used in real-world applications. Thus the development of new algorithms for CFPQ is justified. In this paper, we provide a new CFPQ algorithm which is based on such linear algebra operations as Kronecker product and transitive closure and handles grammars presented as recursive state machines. Thus, the proposed algorithm can be implemented by using high-performance libraries and modern parallel hardware. Moreover, it avoids grammar growth which provides the possibility for queries optimization.
Reconciling Event Structures with Modern Multiprocessors
July 2020
Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis
Context-Free Path Querying with Single-Path Semantics by Matrix Multiplication
June 2020
Arseniy Terekhov, Artyom Khoroshev, Rustam Azimov, Semyon Grigorev
A recent study showed that the applicability of context-free path querying (CFPQ) algorithms with relational query semantics integrated with graph databases is limited because of low performance and high memory consumption of existing solutions. In this work, we implement a matrix-based CFPQ algorithm by using appropriate high-performance libraries for linear algebra and integrate it with RedisGraph graph database. Also, we introduce a new CFPQ algorithm with single-path query semantics that allows us to extract one found path for each pair of nodes. Finally, we provide the evaluation of our algorithms for both semantics which shows that matrix-based CFPQ implementation for Redis-Graph database is performant enough for real-world data analysis.
Modification of Valiant’s algorithm for the string-matching problem
June 2020
Susanina Y.A., Yaveyn A.N., Grigorev S.V.
This paper aims to present Valiant’s algorithm modification, which main advantage is the possibility to divide the parsing table into successively computed layers of disjoint submatrices where each submatrix of the layer can be processed independently. Moreover, our approach is easily adapted for the string-matching problem.
Context-Free Path Querying via Matrix Equations
June 2020
Yuliya Susanina
Repairing and Mechanising the JavaScript Relaxed Memory Model
June 2020
Conrad Watt, Christopher Pulte, Anton Podkopaev, Guillaume Barbier, Stephen Dolan, Shaked Flur, Jean Pichon-Pharabod Shu-yu Guo
Promising 2.0: Global Optimizations in Relaxed Memory Concurrency
June 2020
Sung-Hwan Lee, Minki Cho, Anton Podkopaev, Soham Chakraborty, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis
Optimizing GPU programs by partial evaluation
February 2020
Aleksey Tyurin, Daniil Berezun, Semyon Grigorev
While GPU utilization allows one to speed up computations to the orders of magnitude, memory management remains the bottleneck making it often a challenge to achieve the desired performance. Hence, different memory optimizations are leveraged to make memory being used more effectively. We propose an approach automating memory management utilizing partial evaluation, a program transformation technique that enables data accesses to be pre-computed, optimized, and embedded into the code, saving memory transactions. An empirical evaluation of our approach shows that the transformed program could be up to 8 times as efficient as the original one in the case of CUDA C naïve string pattern matching algorithm implementation.
Compilation of OCaml memory model into Power (In Russian)
December 2019
Egor Namakonov, Anton Podkopaev
Path Querying with Conjunctive Grammars by Matrix Multiplication
December 2019
R. Azimov and S. Grigorev
Path querying with conjunctive grammars is known to be undecidable. There is an algorithm for path querying with linear conjunctive grammars which provides an over-approximation of the result, but there is no algorithm for arbitrary conjunctive grammars. We propose the first algorithm for path querying with arbitrary conjunctive grammars. The proposed algorithm is matrix-based and allows us to efficiently apply GPGPU computing techniques and other optimizations for matrix operations.
Improved Architecture of Artificial Neural Network for Secondary Structure Analysis
November 2019
Semyon Grigorev and Polina Lunina
Property Directed Inference of Relational Invariants
October 2019
D. Mordvinov, G. Fedyukovich
On Satisfiability of Nominal Type Systems With Variance
July 2019
A. Misonizhnik, D. Mordvinov
Bar-Hillel Theorem Mechanization in Coq
June 2019
Sergey Bozhko, Leyla Khatbullina, Semyon Grigorev
The Bar-Hillel theorem states that context-free languages are closed under intersection with a regular set. This theorem has a constructive proof and thus provides a formal justification of correctness of the algorithms for applications mentioned above. Mechanization of the Bar-Hillel theorem, therefore, is both a fundamental result of formal language theory and a basis for the certified implementation of the algorithms for applications. In this work, we present the mechanized proof of the Bar-Hillel theorem in Coq.
Evaluation of the Context-Free Path Querying Algorithm Based on Matrix Multiplication
June 2019
Nikita Mishin, Iaroslav Sokolov, Egor Spirin, Vladimir Kutuev, Egor Nemchinov, Sergey Gorbatyuk, and Semyon Grigorev
The Composition of Dense Neural Networks and Formal Grammars for Secondary Structure Analysis
March 2019
Semyon Grigorev and Polina Lunina
We propose a way to combine formal grammars and artificial neural networks for biological sequences processing. Formal grammars encode the secondary structure of the sequence and neural networks deal with mutations and noise. In contrast to the classical way, when probabilistic grammars are used for secondary structure modeling, we propose to use arbitrary (not probabilistic) grammars which simplifies grammar creation. Instead of modeling the structure of the whole sequence, we create a grammar which only describes features of the secondary structure. Then we use matrix-based parsing to extract features: the fact that some substring can be derived from some nonterminal is a feature. After that, we use a dense neural network to process features.
Path querying on acyclic graphs using Boolean grammars
January 2019
Shemetova E.N., Grigorev S.V.
One of the problems in graph data analysis is querying for specific paths. Such queries are usually performed by means of a formal grammar that describes the allowed edge-labeling of the paths. Path query is said to be calculated using relational query semantics if it is evaluated to triple ((A,v1,v2), such that there is a path from v1 to v2 such that the labels on the edges of this path form a string derivable from the nonterminal A. We focus on the Boolean languages that use Boolean grammars to describe the labeling of paths. Although path querying using relational query semantics and Boolean grammars is known to be undecidable, in this work we propose a path querying algorithm on acyclic graphs which uses relational query semantics and Boolean grammars and approximates the exact solution. To achieve better performance in compare with the naive algorithm, considered classes of graphs were limited to acyclic graphs.
Bridging the Gap Between Programming Languages and Hardware Weak Memory Models
January 2019
Anton Podkopaev, Ori Lahav, Viktor Vafeiadis
Project page: http://plv.mpi-sws.org/imm/
Relational Interpreters for Search Problems
2019
Constructive Negation for MiniKanren
2019
A Survey of Smart Contract Safety and Programming Languages
2019
A. Tyurin, I. Tyulyandin, V. Maltsev, I. Kirilenko, and D. Berezun
Survey on Blockchain Technology, Consensus Algorithms, and Alternative Distributed Technologies
2019
N. Mishin, A. Fefelov, V. Bushev, I. Kirilenko, and D. Berezun
Certified Semantics for miniKanren
2019
Extended Abstract: F# OpenCL Type Provider
September 2018
Kirill Smirenko, Semyon Grigorev
Extended abstract at TyDe 2018 (at ICFP).
Detecting Near Duplicates in Software Documentation
September 2018
D.V. Luciv, D.V. Koznov, G.A. Chernishev, A.N. Terekhov, K.Y. Romanovsky, D.A. Grigoriev
Parser combinators for context-free path querying
September 2018
Ekaterina Verbitskaia, Ilya Kirillov, Ilya Nozkin, Semyon Grigorev
Transparent integration of a domain-specific language for specification of context-free path queries (CFPQs) into a general-purpose programming language as well as static checking of errors in queries may greatly simplify the development of applications using CFPQs. LINQ and ORM can be used for the integration, but they have issues with flexibility: query decomposition and reusing of subqueries are a challenge. Adaptation of parser combinators technique for paths querying may solve these problems. Conventional parser combinators process linear input, and only the Trails library is known to apply this technique for path querying. We demonstrate that it is possible to create general parser combinators for CFPQ which support arbitrary context-free grammars and arbitrary input graphs. We implement a library of such parser combinators and show that it is applicable for realistic tasks.
Relational Programming with memoization and negation (In Russian)
August 2018
E. Moiseenko, A. Podkopaev
Context-free path querying by matrix multiplication
June 2018
Rustam Azimov, Semyon Grigorev
Poster: Duplicate finder toolkit
2018
D.Luciv, D.Koznov, G.Chernishev, H.A. Basit, K.Romanovsky, A.Terekhov
Typed Relational Conversion
2018
Petr Lozov, Andrey Vyatkin, Dmitry Boulytchev
18th International Symposium on Trends in Functional Programming
Improving Refutational Completeness of Relational Search via Divergence Test
2018
Context-Free Path Querying with Structural Representation of Result
December 2017
Semyon Grigorev, Anastasiya Ragozina
There are several solutions for CFPQ, but how to provide structural representation of query result which is practical for answer processing and debugging is still an open problem. In this paper we propose a graph parsing technique which allows one to build such representation with respect to given grammar in polynomial time and space for arbitrary context-free grammar and graph. Proposed algorithm is based on generalized LL parsing algorithm, while previous solutions are based mostly on CYK or Earley algorithms, which reduces time complexity in some cases.
Promising Compilation to ARMv8.3 (In Russian)
December 2017
A. Podkopaev, O. Lahav, V. Vafeiadis
On compilation correctness for a subset of a promising memory model to the ARMv8.3 memory model (In Russian)
December 2017
A. Podkopaev, O. Lahav, V. Vafeiadis
Promising Compilation to ARMv8 POP
June 2017
Anton Podkopaev, Ori Lahav, Viktor Vafeiadis
Compiling untyped lambda calculus to lower-level code by game semantics and partial evaluation
January 2017
Daniil Berezun and Neil D. Jones
Untyped Lambda-Calculus Normalization by Traversals (in Russian)
2017
Berezun D.A.
Complete Head Linear Reduction (in Russian)
2017
Berezun D.A.
Synchronizing constrained horn clauses
2017
Mordvinov, Dmitry, and Grigory Fedyukovich
Verifying Safety of Functional Programs with Rosette/Unbound
2017
Dmitry Mordvinov and Grigory Fedyukovich
TRIK studio: Technical introduction
2017
Mordvinov Dmitry, Yurii Litvinov, and Timofey Bryksin
Certified Grammar Transformation to Chomsky Normal Form in F*
August 2016
Marina Polubelova, Sergey Bozhko, Semyon Grigorev
Relaxed Parsing of Regular Approximations of String-Embedded Languages
June 2016
Ekaterina Verbitskaia , Semyon Grigorev, Dmitry Avdyukhin
We present a technique for syntax analysis of a regular set of input strings. This problem is relevant for the analysis of string-embedded languages when a host program generates clauses of embedded language at run time. Our technique is based on a generalization of RNGLR algorithm, which, inherently, allows us to construct a finite representation of parse forest for regularly approximated set of input strings. This representation can be further utilized for semantic analysis and transformations in the context of reengineering, code maintenance, program understanding etc. The approach in question implements relaxed parsing: non-recognized strings in approximation set are ignored with no error detection.
Operational Aspects of C/C++ Concurrency
June 2016
Anton Podkopaev, Ilya Sergey, Aleksandar Nanevski
Clone detection in reuse of software technical documentation
2016
Koznov, D., Luciv, D., Basit, H.A., Lieh, O.E., Smirnov, M.
Incremental Garbage Collection Library for C++ (in Russian)
2016
E. Moiseenko, D. Berezun
Lexical Analysis of Dynamically Generated String Expressions
2016
Marina Polubelova, Semyon Grigorev
On fuzzy repetitions detection in documentation reuse
2016
Lucive, D.V., Koznov, D.V., Basit, H.A., Terekhov, A.N.
Working Notes: Compiling ULC to Lower-level Code by Game Semantics and Partial Evaluation
2016
Daniil Berezun and Neil D. Jones
Survey on formal methods in robotics
2016
D. A. Mordvinov, Yu. V. Litvinov
A Language-Independent Code Formatting by Syntactic Matching and Templates (In Russian)
October 2015
A.Podkopaev, A.Korovianskii, I.Ozernykh
Generalized Table-based LL-parsing
2015
Ragozina Anastasiya, Grigorev Semyon
Combinators and Type-Driven Transformers in Objective Caml
2015
Dmitry Boulytchev
On development of static analysis tools for string-embedded languages
2015
Marat Khabibullin, Andrei Ivanov, Semyon Grigorev
Polynomial-Time Optimal Pretty-Printing Combinators with Choice
2014
Anton Podkopaev, Dmitry Boulytchev
Precise Garbage Collection for C++ with a Non-Cooperative Compiler
2014
Daniil Berezun, Dmitry Boulytchev
String-embedded Language Support in Integrated Development Environment
2014
Semen Grigorev, Ekaterina Verbitskaia, Andrei Ivanov, Marina Polubelova, and Ekaterina Mavchun
GLR-based Abstract Parsing
2013
Semen Grigorev and Iakov Kirilenko
Document Teaching to write software engineering documents with focus on document design by means of mind maps
2012
Koznov, D.V.
Mind maps merging in collaborative work
2011
Koznov, D., Larchik, E., Pliskin, M., Artamonov, N.
Document Refactoring the documentation of software product lines
2011
Romanovsky, K., Koznov, D., Minchin, L.
Document Towards e-government services in Russia
2011
Koznov, D., Samochadin, A., Azarskov, A., Chevzova, J.
Efficiently Scrapping Boilerplate Code in OCaml
2011
Dmitry Boulytchev, Sergey Mechtaev
Hardware Description Language Based on Message Passing and Implicit Pipelining
2010
Dmitry Boulytchev, Oleg Medvedev
A knowledge management approach for industrial model-based testing
2009
Koznov, D., Malinov, V., Sokhransky, E., Novikova, M.
Computer-supported collaborative learning with mind-maps
2008
Koznov, D., Pliskin, M.
DocLine: A method for software product lines documentation development
2008
Koznov, D.V., Romanovsky, K.Yu.
BURS-based Instruction Set Selection
2006
Dmitry Boulytchev
REAL-IT: Model-Based User Interface Development Environment
2005
A.Ivanov, D.Koznov
Cooking Raw Types in Java
2005
Dmitry Boulytchev, Eugene Vigdorchik
Macroarchitecture Description Language for Hardware/Software Codesign (in Russian)
2004
Dmitry Boulytchev
Macroarchitecture Description for Hardware/Software Codesign (in Russian)
2004
Dmitry Boulytchev
OCL-based automated validation method for UML specifications
2003
Ol'khovich, L., Koznov, D.V.
On Project-Specific Languages and Their Application in Reengineering
2002
Dmitry Boulytchev, Dmitry Koznov, Andrey A. Terekhov
Document A method for recovery and maintenance of software architecture
2001
Koznov, D., Romanovsky, K., Nikitin, A.
An Empirical Study of Retargetable Compilers
2001
Dmitry Boulytchev, Dmitry Lomov
Pattern-matching and Identification of Structural Types in PL/1 (in Russian)
2000
Dmitry Boulytchev
RTST++: Methodology and a CASE tool for the development of information systems and software for real-time systems
1999
Terekhov, A.N., Romanovskii, K.Yu., Koznov, D.V., Dolgov, P.S., Ivanov, A.N.