Towards an Efficient Prolog System by Code Introspection
逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）一些Prolog解释器是基于Warren抽象机（WAM），一个优雅的模型来编译Prolog程序。为了提高性能，提出了优化子句选择、专门化统一、全局分析、本地代码生成和制表等策略。本文提出了一种不同的策略来实现一个高效的Prolog系统，在飞行中创建专门的仿真器。该策略在YAP Prolog系统上进行了实现和评估，实验评估显示了有趣的结果。
2014-05-11 cs.PL
A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs
我们描述了一种方法来验证实现的转换功能的程序，利用高阶表示的语法。在这种方法中，使用遗传Harrop公式的逻辑指定变换。一方面，这些规范直接作为实现，是Lambda Prolog语言中的程序。另一方面，它们可以用作Abella系统的输入，该系统允许我们证明关于它们的属性，从而证明关于实现的属性。我们认为，这种方法是特别有效的实现转换，分析绑定结构。我们通过在Lambda Prolog中描述对这种结构敏感的类型化闭包转换和代码提升等转换的简洁编码，并通过展示如何使用Abella证明其正确性来做到这一点。
2016-01-23 cs.LO cs.PL
An Implementation of the Language Lambda Prolog Organized around Higher-Order Pattern Unification
本论文关注Lambda Prolog的实现，Lambda Prolog是一种高阶逻辑程序设计语言，它支持用二叉树语法方法来表示和操作形式语法对象。Lambda Prolog通过使用类型化的lambda术语作为数据结构来扩展类似Prolog的语言来实现其功能，然后通过高阶统一和一些新的程序级抽象机制来操纵这些数据结构。这些额外的功能提出了新的实现问题，必须充分解决Lambda Prolog作为一个有效的编程工具。我们在这里考虑这些问题，最终提供一个虚拟机和基于编译的实现。一个关键的想法是Lambda Prolog的计算模型的方向围绕一个限制版本的高阶统一，具有良好的算法特性，似乎包括最有趣的应用程序。我们的虚拟机嵌入了沃伦抽象机的结构，是在传统的Prolog实现中使用的这种形式的统一的治疗。一路上，我们对待各种辅助问题，如低层次的表示lambda条款，实施减少这些条款和优化处理的类型计算。我们还开发了Lambda Prolog的实际实现，称为Teyjus版本2。该系统的一个特点是用C语言实现了虚拟机的仿真器，用OCaml语言实现了编译器。我们提出了一种治疗的软件问题，从这种混合的语言在一个系统中，我们讨论了相关的问题，我们的虚拟机仿真器的可移植性在任意架构。最后，我们通过使用该系统进行的实验来评估我们的各种设计思想的有效性。
2009-11-27 cs.PL
Optimizing Queries in a Logic-based Information Integration System
SINTAGMA信息集成系统是一个同时访问几个不同信息源的基础设施。除了为信息源（数据库、Web服务、Web站点、RDF资源、XML文件）提供统一的接口之外，还需要语义集成。语义集成是通过提供一个高级模型和到源模型的映射来实现的。当执行高级模型的查询时，查询被转换为低级查询计划，该计划是回答高级查询的一段Prolog代码。这种转变分两个阶段进行。首先，QueryPlanner生成一个计划，作为表达低级查询的逻辑公式。接下来，查询优化器将此公式转换为可执行的Prolog代码，并根据有关信息源的结构和统计信息对其进行优化。本文讨论了优化算法的主要思想及其实现。
2007-12-19 cs.PL cs.SE
Efficient Groundness Analysis in Prolog
布尔函数可用于表示（约束）逻辑程序中程序变量的基础性，并跟踪它们之间的基础依赖性。在本文中，各种有关的问题进行了调查，有效的Prolog实现的接地分析，集中在域的定布尔函数，def。系统的设计表示的一个抽象域的讨论有关其影响的算法复杂性的域操作;最频繁调用的操作应该是最轻量级的。这种方法被应用到Def，从而在一个新的表示，连同新的算法，其域操作利用以前未开发的属性Def -例如，二次时间蕴涵检查。迭代策略驱动的分析也进行了讨论，并描述了一个简单的，但非常有效的，优化诱导魔术。分析可以直接在Prolog中实现，并且使用非基础表示导致高效，可扩展的工具，即使在最大的基准测试中也不需要扩展。一个广泛的实验评价给出
2002-01-16 cs.PL
Deriving Abstract Semantics for Forward Analysis of Normal Logic Programs
虽然否定作为失败是通过内建谓词来处理的，但在文献中还没有正式地讨论{ \em normal}逻辑程序的前向抽象解释问题！在Prolog中实现的方式。本文提出了一个解决这个问题的方法，推导出两个通用的不动点抽象语义$F^b and $ F^ \diamond { \em正常}逻辑程序的前向抽象解释。$F^b$用于推断程序图中边的数据描述，其中边表示执行控制从其源程序点转移到其目的程序点的可能性。$F^\diamond$源自$F^b$，用于推断文本程序点的数据描述。
1998-11-06 cs.LO cs.PL
Evaluation of the Implementation of an Abstract Interpretation Algorithm using Tabled CLP
CiaoPP是Ciao Prolog系统中逻辑程序的分析器和优化器。它包括PLAI，一个不动点算法的抽象解释的逻辑程序，我们适应使用表格约束逻辑编程。在这种适应中，制表引擎驱动定点计算，而约束求解器处理不同子句的抽象替换的LUB。这简化了代码并提高了性能，因为终止，依赖关系和一些关键操作（例如，分支切换和恢复）由制表引擎直接处理。确定是否已经达到不动点使用语义等价，这可以决定两个语法不同的抽象替换表示抽象域中的同一元素。因此，与使用语法相等的分析器相比，制表分析器可以在更多情况下重用答案。这有助于实现更好的性能，即使考虑到与这些检查相关的额外成本。我们的实现基于Ciao Prolog中的TCLP框架，并且是CiaoPP中初始定点实现的三分之一大小。它的性能进行了评估，通过分析几个程序使用不同的抽象域。这篇论文正在考虑发表在《逻辑程序设计理论与实践》（TPLP）上。
2019-07-31 cs.PL
A scheme for dynamically integrating C library functions into a $λ$Prolog implementation
Teyjus系统通过将程序编译成用于抽象机器的字节码并使用用于机器的模拟器执行该翻译形式来实现高阶逻辑程序设计语言$λ$ Prolog。Teyjus支持许多通过C代码实现的内置关系。在目前的计划中，这些关系是通过包括C程序，实现它们的模拟器和定制的编译器产生的指令调用这样的代码。这种方法有两个缺点。首先，整个库函数集合必须包含在系统中，从而导致比必要的内存占用更大。其次，增强内置谓词的集合需要改变模拟器和编译器的部分，完成这项任务需要这两个子系统的特定知识。该项目分三步解决这些问题。首先，内置函数的代码从模拟器移动到库中，在加载时，由字节码文件中的信息确定的相关部分从库链接到运行时系统。第二，将每个库函数的信息与如何从$λ$ Prolog程序中调用它以及在哪里可以找到它的C代码相关联。最后，修改编译器以使用前面的信息在字节码文件中包含相关的链接指令，并将对内建关系的调用转换为调用动态链接代码的特殊指令。更一般地说，这些想法是能够支持接口在$λ$ Prolog中的“外来功能”在C中实现，也讨论了可能性。
2019-06-03 cs.PL
A Higher-Order Abstract Syntax Approach to the Verified Compilation of Functional Programs
我们认为，功能性程序设计语言的编译器的实现和验证大大简化了采用高阶表示的语法称为高阶抽象语法或HOAS。HOAS的基本思想是使用一种元语言，它为绑定相关概念提供内置的逻辑处理。通过将元语言嵌入到更大的编程或推理框架中，可以将对象语言中的绑定结构的处理吸收到系统的元理论中，从而大大简化整体实现和推理过程。我们在这篇论文中提出并证明了上述论点的有效性的方法来验证执行的编译器转换的函数程序，利用HOAS。在这种方法中，函数程序的转换首先以基于规则的关系规范的形式表达。这些规范被渲染成语言lambda Prolog的程序。一方面，这些程序直接作为实现。另一方面，它们可以用作Abella系统的输入，该系统允许我们证明关于它们的属性，从而证明关于实现的属性。lambda Prolog和Abella都支持使用HOAS方法。因此，它们构成了一个框架，可用于在验证编译中测试HOAS方法的好处。我们用它们来实现和验证一个编译器的代表性的功能程序设计语言，体现了许多编译器的核心，这些语言的转换。在这两个编程和推理阶段，我们展示了如何使用的HOAS方法显着简化了绑定结构的表示，操作，分析和推理。
2017-02-11 cs.LO cs.PL
Typing constraint logic programs
本文提出了一个约束逻辑程序的参数多态和子类型的规定类型系统。这种类型的系统的目的是静态地检测编程错误。它为约束逻辑程序和模块引入了一种类型规则，同时保持了在约束域之间执行通常的转换的能力，以及由于子类型的灵活性而类型化元编程谓词的能力。主语归约的性质表达了规定类型系统与规则类型系统的一致性。执行模型：如果一个程序是“良好类型的”，那么所有从“良好类型的”目标开始的派生都是“良好类型的”。该性质是证明w.r.t.约束程序设计的抽象执行模型，它只通过约束的累积来进行，而w.r.t.一个丰富的执行模型与类型约束的替代。我们描述了我们的实现系统的类型检查和类型推断。本文报告了我们在ISO-Prolog、Sicstus Prolog的约束库和其它Prolog程序上进行类型检查的实验结果。
2004-05-27 cs.PL
Optimizing Abstract Abstract Machines
抽象抽象机（AAM）的技术提供了一个系统的方法来获得可计算的近似值的评估，很容易证明的声音。本文提供了一个补充的分步过程，随后从AAM方法下派生的朴素分析器到有效和正确的实现。该过程的最终结果是比系统推导的分析器有两到三个数量级的改进，使其与手工优化的实现相比具有竞争力，后者计算的结果从根本上来说不太精确。
2013-07-24 cs.PL
An overview of Ciao and its design philosophy
我们提供了一个全面的描述Ciao多范式编程系统，强调其设计和实现背后的一些新的方面和动机。Ciao的一个重要方面是，除了支持逻辑编程（特别是Prolog）之外，它还为程序员提供了大量来自不同编程范式和风格的有用功能，并且每个程序模块都可以随意打开和关闭这些功能（包括Prolog的功能）。因此，给定模块可以使用例如，高阶函数和约束，而另一个模块可能使用赋值、谓词、Prolog元编程和并发。此外，该语言被设计为以简单和模块化的方式进行扩展。Ciao的另一个重要方面是它的编程环境，它提供了一个强大的预处理器（带有相关的断言语言），能够静态地发现非平凡的bug，验证程序是否符合规范，并执行许多类型的优化（包括自动并行化）。此类优化产生的代码与其他动态语言或（实验性）优化编译器甚至静态语言具有高度竞争力，同时保留动态语言的灵活性和交互式开发。这种编译体系结构支持模块化和独立编译。该环境还包括一个功能强大的自动文档管理器和一个单元测试框架，两者都与断言系统紧密集成。本文提供了语言和程序开发环境的非正式概述。它旨在说明设计哲学，而不是详尽无遗，这在一篇期刊论文中是不可能的，而是指向以前的Ciao文献。
2011-02-27 cs.PL
Exploiting Multiple Abstract Call Patterns for Optimizing Run-Time Checks
IMDEA Software Institute（IMDEA软件研究所）；Spanish Council for Scientific Research（西班牙国家研究委员会）
本文通过将断言属性的运行时语义集成到多变量、自顶向下、目标导向的抽象解释算法中，并利用多种推断的调用模式减少运行时检查的属性数量，从而降低开销，在Ciao系统中实现并验证了优于先前技术的性能。
2026-06-16 cs.PL
RVSDG: An Intermediate Representation for Optimizing Compilers
中间表示（IR）是优化编译器的核心，因为程序的表示方式可能会增强或限制分析和转换。合适的IR专注于暴露最相关的信息，并建立不同编译器传递可以依赖的不变量。虽然以控制流为中心的IR似乎是命令式程序设计语言的天然选择，但编译器所需的分析越来越多地转向理解数据依赖关系，并同时在多个抽象层上工作。这在最近的发展中得到了部分证明，例如谷歌提出的MLIR。然而，在通用编译器中严格使用以数据流为中心的IR的可行性和可用性尚未进行评估，因为以前的作品没有提供实际的实现。提出了一种用于优化编译器的区域化值状态依赖图IR。RVSDG是以数据流为中心的IR，其中节点表示计算，边表示计算依赖性，并且区域捕获程序的分层结构。它代表了需求依赖形式的程序，隐式地支持结构化控制流，并在一个单一的IR模型的整个程序。我们提供了一个完整的规范的RVSDG，建设和破坏的方法，以及通过提出死节点和公共节点消除优化的实用程序。我们实现了一个原型编译器，并评估它的性能，代码大小，编译时间和代表性开销。我们的研究结果表明，RVSDG可以作为一个有竞争力的IR优化编译器，同时降低复杂性。
2020-03-17 cs.PL
Ascertaining Uncertainty for Efficient Exact Cache Analysis
静态缓存分析通过以合理但近似的方式确定哪些内存访问导致缓存命中以及哪些导致缓存未命中来表征程序的缓存行为。这些信息在优化编译器、最坏情况下的执行时间分析以及侧信道攻击量化和缓解方面都是有价值的。高速缓存分析通常作为“必须”和“可能”抽象解释的组合来执行，将指令分类为“总是命中”、“总是未命中”或“未知”。分类为“未知”的指令可能会导致命中或未命中，这取决于程序输入或初始高速缓存状态。同样可能的是，它们实际上总是命中或总是未命中，但是高速缓存分析太粗糙而看不到它。我们消除这种不确定性的方法包括（i）一种新颖的抽象解释，能够确定特定指令肯定会在不同路径上导致命中和未命中，以及（ii）一种精确的分析，基于模型检验，消除所有剩余的不确定性，使用抽象解释结果来修剪模型的可扩展性。我们在各种示例上评估了我们的方法;它以合理的成本显着提高了经典抽象解释的精度。
2018-12-20 cs.AR cs.LO cs.PL
Embedded SML using the MLton compiler
在这个扩展的摘要中，我们介绍了我们目前利用标准ML开发嵌入式和实时系统的工作。具体来说，我们详细介绍了我们在修改MLton，一个完整的程序，优化标准ML的编译器，在这种情况下使用的经验。我们主要集中在语言运行时，重新工作的线程子系统和垃圾收集器，以及必要的变化集成MLton生成的程序到一个轻量级的操作系统内核。我们将这些变化与我们以前为多核系统扩展MLton的工作进行了比较和对比，这些工作主要集中在实现可扩展性上。
2016-08-25 cs.PL
A Transformation--Based Approach for the Design of Parallel/Distributed Scientific Software: the FFT
我们描述了一种设计高效的并行和分布式科学软件的方法。这种方法利用序列的机械代数为基础的优化转换。在这项研究中，我们应用我们的方法的FFT，从一个高层次的代数算法描述。抽象的多处理器计划的发展和完善，以指定哪些计算是由每个处理器。然后创建指定处理器上的计算和数据的位置以及处理器之间的数据流的模板。模板以MPI和OpenMP编程风格开发。初步的实验比较使用我们的方法构建的代码与代码从几个标准的科学图书馆表明，我们的代码往往是有竞争力的，有时表现更好。有趣的是，我们的代码在一个目标架构上处理了更大范围的问题大小。
2008-11-15 cs.PL cs.SE
Scoping Constructs in Logic Programming: Implementation Problems and their Solution
本文考虑了逻辑程序设计中目标的泛量化和蕴涵形式。这些新增内容为范围界定提供了逻辑基础，但也带来了新的实现问题。当全称量词和存在量词被允许以混合顺序出现在目标中时，必须修改用于解决存在目标的逻辑变量和统一的设备，以确保尊重量化顺序产生的约束。适当的修改，是基于附加数字标签的常数和变量，并在统一使用这些标签。由此产生的设备是服从一个有效的实施，并可以，事实上，很容易被同化到沃伦抽象机（WAM）的通常机械。在目标中提供含义导致了程序子句被添加到程序中以解决特定子目标的可能性。基于断言和撤回程序条款的天真方案不足以实现此类添加，原因有两个。首先，在回溯时，也有必要支持早期现有程序的复活。第二，隐含目标被量词包围的可能性需要考虑程序子句通过绑定其自由变量的参数化。用于支持这些附加要求的设备也被描述为将这些设备集成到WAM中。进一步扩展的机器概述了处理高阶添加到语言。这里提出的想法是相关的高阶逻辑程序设计语言lambda Prolog的实现。
1998-09-10 cs.PL
