Proceedings of the ACM on Programming Languages, 6(OOPSLA2), 758-785

MINIKANREN 是一种用于逻辑和关系编程的轻量级嵌入式语言。它的许多实用功能来自一种称为交错搜索的独特搜索策略。然而，有了交错搜索，关于逻辑程序的复杂性和性能的传统推理方法就变得无关紧要了。我们确定了一个重要的关键组件调度，它使得 MINIKANREN 的推理非常不同，并提出了一种半自动技术，通过符号执行来估计调度对相当广泛的程序类别的影响。

第 49 届 ACM SIGPLAN 编程语言原理研讨会 (POPL 2012)

Scientific and Technical Journal of Information Technologies, Mechanics and Optics

Syrcose'21

TFPIE-2021

OOPSLA'21 杰出论文奖

OOPSLA

Programming and Computer Software Journal

我们为关系型编程语言 miniKanren 提出了一种新的、公平的、合取评价策略。与最初的左偏合取不同，我们的方式基于关系定义的内在属性控制合取执行的顺序。我们给出了合取公平性的形式化研究和实际评估，在性能和收敛方面都有了实质性的提高。

SEIM-2021

ICPP-2021

我们给出了关系型编程语言 MINIKANREN 的形式化语义研究。首先，我们建立了与确定逻辑程序的最小 Herbrand 模型相对应的指称语义。其次，给出了 MINIKANREN 实现的显著特征 -- 对交错进行建模的操作语义，并从指称语义的角度证明了它的可靠性和完整性。我们的开发得到了 CoQ 规范的支持，可以从该规范中提取引用解释器。我们还从主要结果中得到了 SLD 解析的认证语义（和引用解释器），并证明了它的可靠性。

我们提出了一种完全声明性的方式来综合基于关系编程的模式匹配构造实现，关系编程是约束逻辑编程的一种特定形式。我们的方式基于模式匹配的高级语义和中级实现语言的语义的关系表示。原则上，这种选择使我们的方式具有很强的可扩展性，因为我们只需要修改高级语义，就可以合成模式匹配新功能的实现。我们对部分取自现有文献的一组小样本的评估表明，我们的框架能够快速合成最优实现。然而，我们对一些人工基准的深度压力评估表明，未来还需要改进。

上下文无关路径查询 (CFPQ) 通过允许上下文无关语法作为路径约束来扩展常规路径查询 (RPQ)。CFPQ 算法正在积极开发，但 J. Kuijpers 等人最近得出结论，现有算法的性能不足以用于实际应用。因此，开发新的 CFPQ 算法是合理的。本文提出了一种新的 CFPQ 算法，该算法基于克罗内克积和传递闭包等线性代数运算，并处理以递归状态机表示的语法。因此，提出的算法可以通过使用高性能库和现代并行硬件来实现。此外，它避免了语法增长，从而为查询优化提供了可能性。

ADBIS 2020. Advances in Databases and Information Systems. 计算机科学讲义。

正则表达式在 SPARQL 属性路径中被用来查询 RDF 图。然而，正则表达式只能定义最有限的一类语言，称为正则语言。上下文无关语言是一个包含所有常规语言的更广泛的类。没有上下文无关表达式来定义它们，因此有必要编写语法。我们提出了一个正则表达式的扩展，称为递归表达式，以支持上下文无关语言的子集的定义。因此，我们的工作目标是提供简单的运算符，使语言的定义尽可能地接近于上下文无关语言。

2020 年 ADBIS、TPDL 和 EDA 共同研讨会与博士联盟

The European Conference on Object-Oriented Programming (ECOOP)

上下文无关路径查询 (CFPQ) 被广泛用于不同领域的图结构数据分析。由于输入数据的大小通常很大，因此开发高效的 CFPQ 算法至关重要。我们展示了如何将 CFPQ 评估简化为求解 R 上的矩阵方程组（一个存在高性能解决方案的问题）。此外，我们还展示了我们的方式对现实世界数据分析的适用性。

2020 年 ACM SIGMOD 数据管理国际会议论文集

本文提出了 Valiant 算法的改进，其主要优点是可以将解析表划分为连续计算的不相交的子矩阵层，其中每一层的子矩阵都可以独立处理。此外，我们的方式很容易适用于字符串匹配问题。

系统编程学会论文集

最近的一项研究表明，由于现有解决方案的性能低下且内存消耗大，将关系查询语义与图形数据库相结合的上下文无关路径查询 (CFPQ) 算法的适用性受到限制。在这项工作中，我们使用适当的高性能线性代数库实现了一个基于矩阵的 CFPQ 算法，并将其与 RedisGraph 图形数据库集成在一起。此外，我们还介绍了一种新的具有单路径查询语义的 CFPQ 算法，，使我们能够为每对节点提取一条找到的路径。最后，我们在这两种语义下对我们的算法进行了评估，结果表明基于矩阵的 Redis-Graph 数据库的 CFPQ 实现对于现实世界的数据分析足够高效。

GRADES-NDA'20：第 3 届图形数据管理经验与系统 (GRADES) 与网络数据分析 (NDA) 联合国际研讨会论文集

41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020)

41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020)

虽然 GPU 利用率可以将计算速度提高几个数量级，但内存管理仍然是一个瓶颈，使其经常成为实现所需性能的挑战。因此，利用了不同的内存优化方案来使内存得到更有效的利用。我们提出了一种利用部分评估实现内存管理自动化的方式，这是一种程序转换技术，可以预先计算、优化数据访问并将其嵌入到代码中，从而节省内存事务。对该方式的实证评估表明，在 CUDA C 朴素字符串模式匹配算法实现的情况下，转换后程序的效率可以达到原始程序的 8 倍。

PPoPP '20：第 25 届 ACM SIGPLAN 并行编程原理与实践研讨会论文集

ISP RAS 会议记录

众所周知，使用合取语法的路径查询不可判定。有一种使用线性合取语法的路径查询算法，它提供了对结果的过近似，但还没有适用于任意合取语法的算法。我们提出了第一种基于任意合取语法的路径查询算法。所提出的算法是基于矩阵的，使我们能够有效地应用 GPGPU 计算技术和其他针对矩阵运算的优化。

Programming and Computer Software

BMC Bioinformatics

第 19 届计算机辅助设计中的形式方法国际会议论文集，FMCAD 2019

33rd European Conference on Object-Oriented Programming (ECOOP 2019)

最近提出的基于矩阵乘法的上下文无关路径查询算法 (CFPQ) 将性能最关键的部分卸载到布尔矩阵乘法上。因此，通过现代并行硬件和软件实现 CFPQ 的高性能是可能的。在本文中，我们提供了该算法的不同实现在真实数据和最坏情况下的合成数据上的经验性能比较结果。

第 2 届图形数据管理经验与系统 (GRADES) 与网络数据分析 (NDA) 联合国际研讨会论文集

Bar-Hillel 定理指出，上下文无关语言在与正则集相交的情况下是封闭的。该定理具有构造性证明，从而为上述应用提供了算法正确性的形式证明。因此，Bar-Hillel 定理的机械化既是形式语言理论的一个基本结果，也是算法在应用中得到认证实现的基础。在这项工作中，我们在 Coq 中提出了 Bar-Hillel 定理的机械化证明。

Logic, Language, Information, and Computation

我们提出了一种将形式语法和人工神经网络相结合的方法来处理生物序列。形式语法编码序列的二级结构，神经网络处理突变和噪声。与经典的方式相反，当使用概率语法进行二级结构建模时，我们建议使用任意（非概率）语法，这样能够简化语法创建。我们没有对整个序列的结构进行建模，而是创建了一个只描述二级结构特征的语法。然后，我们使用基于矩阵的分析来提取特征：某个子字符串可以从某个非终端派生出来，这就是一个特征。之后，我们使用密集神经网络来处理特征。

第 12 届生物医学工程系统与技术国际联合会议论文集 - BIOINFORMATICS

图形数据分析中的其中一个问题是查询特定路径。此类查询通常通过描述允许的路径边标记的形式语法来执行。如果路径查询被评估为三重（A、v1、v2），使得存在一条从 v1 到 v2 的路径，使得该路径边缘上的标签形成可从非终端 A 派生的字符串，则称该路径查询是使用关系查询语义评估的。我们重点介绍使用布尔语法来描述路径标记的布尔语言。虽然已经知道使用关系查询语义和布尔语法进行路径查询不可判定，但在本文中，我们提出了一种基于非循环图的路径查询算法，该算法使用了关系查询语义和布尔语法，并逼近了精确解。为了获得比朴素算法更好的性能，所考虑的图类仅限于无环图。

系统编程学会论文集

2019 年 miniKanren 与关系型编程研讨会论文集

SEIM-19

第 13 届软件工程春夏青年研究员座谈会 (SYRCoSE 2019) 初步论文集，2019 年 5 月 29日 - 31 日 - 俄罗斯联邦，萨拉托夫

2019 年 miniKanren 与关系型编程研讨会论文集

2019 年 miniKanren 与关系型编程研讨会论文集

Programming and Computer Software

TyDe 2018（于 ICFP）的扩展摘要。

将用于规范上下文无关路径查询 (CFPQ) 的特定领域语言透明地集成到通用编程语言中，并对查询中的错误进行静态检查，可以极大地简化使用 CFPQ 的应用程序的开发。LINQ 和 ORM 可以用于集成，但它们在灵活性方面存在问题：查询分解和子查询的重用是挑战。采用解析器组合子技术进行路径查询可以解决这些问题。传统的解析器组合子能够处理线性输入，并且已知只有 Trails 库将该技术应用于路径查询。我们证明了为 CFPQ 创建支持任意上下文无关语法和任意输入图的通用解析器组合子是可能的。我们实现了一个这样的解析器组合子库，并表明它适用于实际任务。

第 9 届 ACM SIGPLAN Scala 国际研讨会论文集

NTV SPbSTU

GRADES-NDA‘18 首届 ACM SIGMOD 图形数据管理经验与系统 (GRADES) 与网络数据分析 (NDA) 联合国际研讨会论文集

18th International Symposium on Trends in Functional Programming

第 20 届声明式编程原理与实践国际研讨会论文集

2016 年 ML/OCAML 论文集

40th ACM/IEEE International Conference on Software Engineering, ICSE 2018

NTV SPbSTU

CFPQ 有多种解决方案，但如何为查询结果提供实用的结构化表示，以便于答案处理和调试，仍是一个有待解决的问题。在本文中，我们提出了一种图分析技术，它允许人们在多项式时间和空间上为任意上下文无关语法和图建立关于给定语法的表示。所提出的算法基于泛化的 LL 解析算法，而以往的算法大多基于 CYK 或 Earley 算法，这在某些情况下降低了时间复杂度。

俄罗斯第 13 届中东欧软件工程会议论文集 (CEE-SECR ‘17)

ISP RAS 会议记录

arXiv

The European Conference on Object-Oriented Programming (ECOOP)

2017 年 ACM SIGPLAN 部分评估和程序操纵研讨会论文集

圣彼得堡州立理工大学学报。Computer Science. 电信与控制系统

Izvestia vuzov. North Caucasus Region. Technical Sciences, 2017, 第 4 期，第 5-12 页

系统编程学会论文集

arXiv

我们提出了一种对常规输入字符串集进行语法分析的技术。当主机程序在运行时生成嵌入语言的子句时，该问题与字符串嵌入语言的分析相关。我们的技术基于 RNGLR 算法的泛化，该算法本质上允许我们为规则近似的输入字符串集构造解析森林的有限表示。这种表示可以进一步用于再工程、代码维护、程序理解等上下文中的语义分析和转换。所述方式实现了松弛解析：忽略近似集中未识别的字符串，不进行错误检测。

Perspectives of System Informatics

Systems and Means of Informatics

META 2016 第五届国际 Valentin Turchin 元计算研讨会

SEIM-16

NTV SPbSTU 4 (224)

Systems and Means of Informatics

Science of Computer Programming

俄罗斯第 11 届中东欧软件工程会议论文集

第 9 届纪念 Andrei Ershov 国际系统信息学展望会议论文集

2014 年俄罗斯第 10 届中东欧软件工程会议论文集

俄罗斯第 10 届中东欧软件工程会议论文集

俄罗斯第 9 届中东欧软件工程会议论文集

机器学习研讨会

2010 年东西方设计与测试研讨会论文集

第 6 届纪念 Andrei Ershov 国际系统信息学展望会议论文集

面向对象语言多范式编程研讨会

System Informatics

System Programming

System Programming

欧洲软件维护与再工程会议论文集，CSMR 995802，pp. 177-185

第 4 届纪念 Andrei Ershov 国际系统信息学展望会议论文集

Automated Reengeneering of Programs, Saint Petersburg