The BinProlog Experience: Architecture and Implementation Choices for Continuation Passing Prolog and First-Class Logic Engines
我们描述了BinProlog系统的编译技术，运行时系统和它的扩展支持一流的逻辑引擎，同时提供了一个简短的历史，它的一些较新的重新实现的细节，以及在他们的设计中涉及的最重要的架构选择的概述。与传统的WAM实现的差异，我们解释BinProlog的编译技术，它取代了WAM与简化的连续传递运行时系统（“BinWAM”）的关键细节，基于映射的完整Prolog二进制逻辑程序。这之后是使用“tag-on-data”表示的术语压缩技术的描述。后来的衍生产品，基于Java的Jinni Prolog编译器和最近开发的Lean Prolog系统用一流的逻辑引擎改进了BinProlog架构，通过使用Interactor接口使其通用。概述了他们的应用程序，重点是在源代码级别表达各种Prolog内置和扩展的能力，涵盖了这些新的发展。
2011-02-06 cs.PL
Lock-free atom garbage collection for multithreaded Prolog
动态语言（如Prolog或Lisp及其衍生物）的运行时系统包含一个符号表，在Prolog中通常称为原子表。一个简单的动态哈希表曾经是实现这个表的一个合适的方法。随着Prolog在24x7服务器进程中的流行，我们需要处理原子垃圾回收和对原子表的并发访问。经典的基于锁的实现，以确保原子表的一致性伸缩性差，停止世界的方法来实现原子垃圾回收很快成为瓶颈，使Prolog不适合软实时应用程序。在本文中，我们描述了一种使用无锁技术的原子表的新颖实现，其中原子表即使在原子垃圾回收期间也保持可访问性。仅依赖于CAS（比较和交换），而不是外部库，实现是简单和可移植的。正在考虑接受TPLP。
2016-08-02 cs.PL
Description and Optimization of Abstract Machines in a Dialect of Prolog
为了实现有竞争力的性能，Prolog和相关语言的抽象机器最终变得庞大而复杂，并在设计和实现级别都包含复杂的优化。同时，效率方面的考虑使得有必要在其实现中使用低级语言。这使得它们很难编码、优化，尤其是维护和扩展。用高级语言编写抽象机器（和辅助代码）可以帮助驯服这种固有的复杂性。我们展示了如何使用Prolog的一个有效的虚拟机的最基本的组件的语义可以描述（的变体）Prolog。然后将这些描述编译成C语言，并组装成一个完整的字节码仿真器。由于所使用的语言的高级别及其与Prolog的接近性，抽象机器描述可以使用标准Prolog编译和优化技术相对容易地进行操作。我们还展示了如何通过有选择地应用程序转换，我们获得抽象的机器实现，其性能可以匹配，甚至超过最先进的，高度调整的，手工制作的仿真器。
2014-11-20 cs.PL
More declarative tabling in Prolog using multi-prompt delimited control
几个Prolog实现包括一个制表设施，一个替代的解决策略，使用memoisation，以避免冗余的重复计算。直到最近，制表还需要底层Prolog引擎中的低级支持，或者广泛的程序transmittance（de Guzman等人，2008年）。另一种方法是增加Prolog与低级别的支持连续捕获控制操作符，特别是定界的延续，这已经在函数编程领域进行了研究，并发现能够支持各种各样的计算效果，否则声明性语言。本技术报告描述了基于Schrijvers等人（2013）最近引入的Prolog分隔控制运算符的SWI Prolog中的制表实现。与之前使用分隔控件的SWI Prolog制表实现（Desouter等人，2015），这种方法基于Johnson（1995）的函数记忆解析器组合子，更接近Prolog的声明性核心，需要更少的代码，并且能够从表格谓词系统中增量地交付解决方案（而不是在将任何解决方案交付给程序的其余部分之前找到所有解决方案）。一组基准测试表明，少量精心针对性的优化产生的性能在Desouter等人的优化版本的约2倍之内。的系统目前包含在SWI Prolog中。
2017-08-24 cs.DS cs.PL
A Prolog-based Environment for Reasoning about Programming Languages (Extended abstract)
ECLAIR是一个基于Prolog的原型系统，旨在为程序设计语言分析和实现工具的研究、开发和评估提供一个功能完整的环境。在本文中，我们勾画了系统的总体结构，概述了其组件的主要方法和技术。我们还讨论了Prolog作为系统实现语言的适当性：除了突出其优点外，我们还指出了一些潜在的弱点，暗示了可能的解决方案。
2007-11-02 cs.PL cs.SE
ITE: A Lightweight Implementation of Stratified Reasoning for Constructive Logical Operators
Simula Research Laboratory（西穆拉研究实验室）
约束编程（CP）是一种功能强大的声明式编程范式，其中推理和搜索交织在一起，以找到各种类型约束系统的可行和最佳解决方案。然而，在CP中处理具有构造性信息的逻辑连接符是非常困难的。本文提出了一个轻量级的逻辑连接词分层构造性推理的实现-如果则否则（ITE）。分层是为了应对从嵌套和组合逻辑运算符构造信息的组合爆炸的风险。ITE是一个建立在SICStus Prolog clp（fd）之上的开源库，它提出了各种运算符，包括构造性析取和否定，构造性蕴涵和条件。这些算子可以用来表达全局约束，并在约束过滤过程中从构造性推理中受益，以实现更多的域修剪。尽管ITE与某些全局约束实现中可用的专用过滤算法相比没有竞争力，但其表达能力允许用户轻松定义具有强大演绎功能的优化约束。我们的扩展实验结果表明，ITE是更有效的比现有的通用方法，处理逻辑约束系统在有限域。
2020-06-22 cs.AI
On the Performance of Bytecode Interpreters in Prolog
Prolog语言的语义和递归执行模型使得语言解释器可以很自然地以AST（Abstract StringTree）解释器的形式表示，其中执行遵循程序的树表示。另一种实现技术是字节码解释器。这些解释器在评估之前将程序转换为紧凑和线性的表示，通常被认为更快，更好地利用资源。本文讨论了在Prolog语言中解释器控制流的不同表示方法，并给出了AST和字节码解释器的几种实现。在一个简单的语言设计用于此目的，我们评估是否最好的技术已知的命令式语言是适用于Prolog和如何以及他们的表现。我们的最终目标是评估Prolog中的解释器设计是最有效的，因为我们打算将这些结果应用到更复杂的语言中。然而，我们相信本文中的分析具有更普遍的意义。
2020-08-28 cs.PL
Interning Ground Terms in XSB
本文介绍了在XSB表式Prolog系统中实现基项的存储。这与hash-consing的概念有关。我描述了实习原子的概念，并讨论了实习地面结构化条款周围的问题，激发为什么制表Prolog系统可能会改变传统的Prolog系统的成本效益权衡。本文详细介绍了XSB表式Prolog系统中实习基本术语的实现，并给出了它的一些性能特性。这个实现实现达到了Zhou和Have的效果，但针对XSB的表示进行了调整，并且可以说更简单。
2013-07-17 cs.PL
Representation Sharing for Prolog
表示共享可以通过在重复项之间共享一个表示来减少程序的内存占用。函数式编程系统中最常见的表示共享实现称为散列consing。在Prolog的上下文中，表示共享很少受到关注。一些当前的技术，处理表示共享的审查。新的贡献是：（1）用于{ \em findall/3}的{\em输入共享}的简单实现;（2）在运行时引入表示共享的{ \em sharer}模块的描述。它们的实现在由hProlog实现的WAM的上下文中示出。两者都可以适用于任何WAM类Prolog实现。共享器独立于垃圾收集器工作，但可以使其与垃圾收集器协作。基准测试结果表明，共享器的成本与堆垃圾收集器相当，其有效性高度依赖于应用程序，并且其策略必须根据收集器进行调整。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
2011-06-30 cs.PL
Bringing GNU Emacs to Native Code
Emacs Lisp（Elisp）是Emacs文本编辑器家族使用的Lisp方言。GNU Emacs目前可以执行Elisp代码，无论是解释的还是编译成字节码后的字节解释的。在这项工作中，我们将讨论一个优化的Elisp针对本机代码的编译器方法的实现。本机编译器使用字节编译器的内部表示作为输入，并利用libgccjit使用GNU编译器集合（GCC）基础设施实现代码生成。生成的可执行文件存储为二进制文件，可以动态加载和卸载。该编译器的大部分功能都是用Elisp本身编写的，包括几个优化通道，以及一个与GNU Emacs核心和libgccjit接口的C后端。虽然仍在进行中，但我们的实现能够引导功能Emacs并编译所有词法范围的Elisp文件，包括整个GNU Emacs Lisp Package Archive（ELPA）。在一组小型基准测试中，本机编译的Elisp相对于等效字节码显示出从2.3倍到42倍的性能提升。
2020-04-06 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
Automatic Differentiation using Constraint Handling Rules in Prolog
自动微分是一种技术，它允许程序员通过组合大范围的数值和计算原语来定义数值计算，并使底层系统支持计算结果相对于其任何输入的偏导数，而不进行任何有限差分近似，也不操纵表示计算的大型符号表达式。本文介绍了一种新的方法，反向模式自动微分使用约束逻辑编程，具体地说，约束处理规则（约束处理规则）库的SWI Prolog，在一个非常小的（50行代码）的实现。当应用于概率语法中参数学习的内部-外部算法的基于微分的实现时，基于TensorFlow的实现大大优于两个著名的优化可微函数的框架Theano和TensorFlow。
2017-06-01 cs.MS cs.PL cs.SC
Using Prolog for Transforming XML Documents
程序设计语言Prolog的支持者都认为Prolog更适合转换XML文档，就像其他成熟的技术和语言一样，比如XML。为了澄清这一立场，这项工作提出了一个tuProlog风格的解释器，用于将XML文档解析为Prolog内部列表，反之亦然，用于将列表序列化为XML文档。基于这个实现，下面比较了prolog和Prolog。首先，研究了标准，如考虑的语言特征的可重用性和可表达性。这些标准已得到验证。其次，它是评估时，Prolog区分输入和输出参数的可逆转换。
2021-04-23 cs.IR cs.PL cs.SE
Portability of Prolog programs: theory and case-studies
Prolog程序的（非）可移植性被广泛认为是该语言缺乏接受度的一个重要因素。自1995年以来，该语言的核心由ISO标准13211-1覆盖。自2007年以来，YAP和SWI-Prolog已经建立了一个基本的兼容性框架。本文介绍并评价了该框架。该框架的目标是在两个系统上运行相同的代码，而不是迁移应用程序。我们表明，今天，爱丁堡/Quintus派生Prolog实现的家庭内的可移植性是足够好的，以允许维护便携式现实世界的应用程序。
2010-09-20 cs.PL
The Language Features and Architecture of B-Prolog
B-Prolog是标准Prolog语言的高性能实现，具有多个扩展，包括匹配子句、事件处理的动作规则、有限域约束求解、数组和哈希表、声明性循环构造和制表。B-Prolog系统基于TOAM体系结构，其与WAM的不同之处主要在于（1）参数通过堆栈老式地传递，（2）每个谓词调用仅使用一个帧，以及（3）提供用于编码匹配树的指令。最新的建筑，称为小TOAM，与WAM的不同之处在于，它不使用用于参数或临时变量的寄存器，并提供用于编码谓词调用的可变大小指令。本文概述了语言的特点，并详细描述了TOAMJr.体系结构，包括对操作规则和制表的体系结构支持。
2011-03-04 cs.PL
Extending the logical update view with transaction support
由于数据库更新视图在Prolog ISO标准中被标准化，因此所谓的逻辑更新视图在所有主动维护的Prolog系统中都可用。虽然这个更新视图提供了一个定义良好的更新语义，并允许有效地处理动态代码，但它无助于维护动态数据库的一致性。随着多线程的引入和Prolog在连续运行的服务器应用程序中的部署，动态数据库的一致性变得非常重要。在本文中，我们提出了对支持事务的逻辑更新视图的基于生成的实现的扩展。基于生成的事务已经根据SWI-Prolog RDF存储中的描述实现。本文的目的是激励交易，概述了实现和生成讨论的理想的语义和接口实现之前。
2013-01-31 cs.DB cs.PL
Customisable Handling of Java References in Prolog Programs
用于组合以不同语言范式编写的程序的集成技术有助于以最适合其任务的语言实现专用模块。在Java-Prolog集成的情况下，一个已知的问题是Prolog端对Java对象的引用的正确表示。要解决这一问题，需要从多个方面进行考虑，包括引用表示、表示的不透明性、身份保持、引用寿命和跨语言转换策略的范围。本文提出了一种方法，解决所有这些方面，概括和建立在Prolog中的外国参考文献的现有表示模式，并从其他领域中发现的类似的中间语言表示技术中汲取灵感。我们的方法通过对Prolog引擎与Java的交互做一些假设（例如，嵌入或作为外部进程执行）。我们验证我们的工作扩展JPC，一个开源的集成库，支持我们的方法的功能。我们的JPC库目前通过驱动程序与三种不同的开源Prolog引擎（SWI，YAP和XSB）兼容。出现在逻辑编程理论与实践（TPLP）中。
2014-05-29 cs.PL
Prolog Server Pages
Prolog Server Pages（PSP）是一种基于Prolog的脚本语言，可以嵌入到HTML文档中。要运行PSP应用程序，需要一个Web服务器，一个Web浏览器和一个PSP解释器。代码由解释器在服务器端（Web服务器）执行，输出（连同嵌入PSP代码的html代码）发送到客户端（浏览器）。当前的实现支持Apache Web Server。我们实现了一个处理PSP文件的Apache Web服务器模块，并将结果（一个html文档）发送到客户端。PSP支持GET和POST HTTP请求。它还提供了使用http cookie的方法。
2006-03-26 cs.NI cs.PL
Secure Prolog-Based Mobile Code
LogicWeb移动代码由嵌入在Web页面中的类似于Prolog的规则组成，从而为这些页面添加逻辑编程行为。由于LogicWeb程序是从外部主机下载并在本地执行的，因此需要保护客户机免受错误或恶意代码的影响。安全模型对于使LogicWeb移动代码安全执行至关重要。本文提出了这样一个模型，它支持不同的信任级别的程序使用不同的资源访问策略。该模型的实现源于LogicWeb语言的扩展操作语义，它提供了安全的精确含义。
2004-06-07 cs.PL
Disjunctive Delimited Control
定界控制是一种用于程序设计语言扩展的强大机制，它是最近为Prolog提出的（并在SWI-Prolog中实现）。通过从语言内部操纵程序的控制流，它可以实现强大的功能，如制表，而无需修改Prolog引擎的内部。然而，它目前的公式是不够的：它没有捕捉到Prolog的独特的非确定性的性质，允许多种方式来满足一个目标。本文充分拥抱Prolog的非确定性与一个新的接口分离定界控制，这使程序员不仅控制顺序（合取）控制流，但也超过了非确定性控制流。我们提供了一个元解释器，保守地扩展Prolog与分隔控制，并表明它使一系列典型的Prolog功能和扩展，现在在库级别：findall，削减，分支定界优化，概率编程，。. .这篇论文正在考虑发表在《逻辑程序设计理论与实践》（TPLP）上。
2023-03-07 cs.PL
Interactive Problem Solving in Prolog
本文提出了一种环境，解决Prolog问题，已实现为虚拟实验室VILAB的一个模块。在问题解决过程中，学习者得到快速的自适应反馈。因此，分析学习者的行动，系统建议使用适当的辅助谓词，也将检查适当的实施。该环境的重点是VILAB中的鲁棒性和集成。
2006-11-03 cs.CY cs.HC cs.PL
Disjunctive Delimited Control
定界控制是一种用于程序设计语言扩展的强大机制，它是最近为Prolog提出的（并在SWI-Prolog中实现）。通过从语言内部操纵程序的控制流，它可以实现强大的功能，如制表，而无需修改Prolog引擎的内部。然而，它目前的公式是不够的：它没有捕捉到Prolog的独特的非确定性的性质，允许多种方式来满足一个目标。本文充分拥抱Prolog的非确定性与一个新的接口分离定界控制，这使程序员不仅控制顺序（合取）控制流，但也超过了非确定性控制流。我们提供了一个元解释器，保守地扩展Prolog与分隔控制，并表明它使一系列典型的Prolog功能和扩展，现在在库级别：findall，削减，分支定界优化，概率编程，…
2021-08-06 cs.LO cs.PL
The Janus System: Multi-paradigm Programming in Prolog and Python
本文介绍Janus系统，它紧密集成Prolog和Python于单一进程，实现双向数据转换和每秒数十万次跨语言调用，已用于商业应用，并易于移植到其他Prolog系统。
2023-08-30 cs.LO cs.PL
Code Staging in GNU Guix
GNU Guix是一个“功能性”包管理器，它建立在Nix的早期工作之上。Guix将包和操作系统服务等高级抽象实现为嵌入在Scheme中的特定领域语言（DSL）。它还在Scheme中实现构建操作和操作系统编排。这导致了一个多层编程环境，其中嵌入的代码片段被分级以供最终执行。本文介绍了G-表达式或“gexps“，分期机制，我们设计的Guix。我们解释了从传统Lisp S表达式到G表达式的旅程，G表达式通过上下文信息增强了前者，并确保了健康的代码分期。我们将讨论gexp的实现，并报告我们在各种操作系统用例中使用它们的经验从包构建过程到系统服务。Gexp提供了一种新颖的方法，用一种单一的多层语言涵盖操作系统配置的许多方面，同时促进代码重用和代码共享。
2017-09-04 cs.PL cs.SE
Sequence-Based Abstract Interpretation of Prolog
针对现有Prolog抽象解释框架无法覆盖部分控制结构的问题，提出基于替换序列、可处理深度优先搜索与cut操作符的新框架，证明其适配传统抽象域且可涵盖此前的确定性分析工作，实验验证了有效性。
2000-10-19 cs.LO cs.PL
Translating Nondeterministic Functional Language based on Attribute Grammars into Java
基于知识的系统适合于实现需要特定领域专家知识的高级功能，而知识表示语言及其支持环境对于实现这样的系统是必不可少的。虽然Prolog在实现这样的支持环境方面是有用和有效的，但是语言与其他实现语言（例如Java）的互操作性通常是实际应用开发中的重要问题。本文介绍了将一种基于属性文法的非确定性函数语言知识表示语言翻译成Java的技术。翻译是基于二进制化和技术提出的Prolog到Java的翻译，虽然语义是不同的Prolog。引入连续单元有效地处理连续问题，同时利用变量的单向赋值特性简化了回溯过程中的变量和寄存器管理。用该语言编写的实验翻译器成功地生成了Java代码，实验结果表明，对于非确定性程序，生成的代码比Prolog Cafe快25倍以上，对于确定性程序，生成的代码比Prolog Cafe快2倍以上。对于不确定性程序，生成的代码也比B-Prolog快2倍以上。
2011-09-03 cs.PL
Prime Path Coverage in the GNU Compiler Collection
本研究在GCC 15中实现主路径覆盖支持，证明其包含MC/DC，通过后缀树优化主路径枚举算法降低时间复杂度，可高效追踪路径并以语言无关方式实现路径插桩与覆盖报告。
2025-04-25 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
On the Implementation of the Probabilistic Logic Programming Language ProbLog
K.U. Leuven（鲁汶大学）
在过去的几年里，人们对概率逻辑学习和统计关系学习领域的兴趣激增。在这一努力中，许多概率逻辑被开发出来。ProbLog是Prolog最近的一个概率扩展，其动机是挖掘大型生物网络。在ProbLog中，事实可以用概率来标记。这些事实被视为相互独立的随机变量，表明这些事实是否属于随机抽样程序。可以向ProbLog程序提出不同类型的查询。我们介绍的算法，使这些查询的有效执行，讨论他们的实施上的YAP-Prolog系统，并评估其性能的背景下，大型网络的生物实体。
2010-06-23 cs.LG cs.LO cs.PL
ECLiPSe - from LP to CLP
ECLiPSe是一个基于Prolog的编程系统，旨在开发和部署约束编程应用程序。它也用于教学组合问题解决的大多数方面，例如问题建模，约束规划，数学规划和搜索技术。它使用扩展的Prolog作为其高级建模和控制语言，辅以几个约束求解器库，第三方求解器接口，集成开发环境和嵌入主机环境的接口。本文讨论了语言扩展，实现方面，组件和工具，我们认为相关的方式从逻辑编程约束逻辑编程。
2010-12-20 cs.PL
Mapping Objects to Persistent Predicates
Prolog逻辑程序设计在许多需要存储知识的系统中被广泛用于提供持久性。用于供应持久性的Prolog编程语言的一些实现具有与其他程序设计语言的双向接口，总体上具有面向对象的编程语言。目前，缺少用于系统开发的工具和框架，这些工具和框架以简单和敏捷的形式使用逻辑谓词持久性。更具体地说，目前需要一个面向对象和逻辑持久性提供程序，允许在主存中操作对象，并且该对象的持久性具有逻辑编程谓词方面。目前的工作介绍了一个面向对象和逻辑持久性提供者的支持对象的序言声明性映射的替代。所提出的替代方案包括逻辑编程谓词与面向对象方法的对应关系，其中对于逻辑编程的每个元素，一个面向对象的元素使其相互作用。逻辑程序设计谓词的面向对象表示提供了对组成知识的元素进行操作的便利。
2017-05-01 cs.LO cs.PL cs.SE
Backjumping is Exception Handling
ISO Prolog提供了catch和throw来实现异常处理的控制流。这颗珍珠表明，接球和投掷是不显眼的服从执行背跳。事实上，它们具有所需的精确语义：将搜索倒回到特定点，并将保留的术语携带到该点。这些属性的效用是通过实现的图形着色与backjumping和backjumping SAT求解器，适用于冲突驱动的子句学习。
2020-08-11 cs.PL
Natlog: a Lightweight Logic Programming Language with a Neuro-symbolic Touch
University of North Texas（北德克萨斯大学）
我们介绍Natlog，一个轻量级的逻辑程序设计语言，共享Prolog的统一驱动的执行模型，但具有简化的语法和语义。我们的概念验证Natlog实现紧密嵌入在基于Python的深度学习生态系统中，专注于基础术语数据集的内容驱动索引。作为我们的符号索引算法的覆盖，相同的功能可以委托给神经网络，为Natlog的解析引擎提供基础事实。我们的开源实现可以在https://pypi.org/project/natlog/上以Python包的形式获得。
2021-09-17 cs.AI cs.LG cs.LO
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
Reversible Language Extensions and their Application in Debugging
有一系列的方法和技术可用于指导语言扩展和领域特定语言的设计和实现。一种简单而强大的技术是基于跨基本语言的编译通道交错的源到源转换。尽管是一种成功的方法，但它的主要缺点是输入源代码在过程中丢失。当考虑到程序开发的整个工作流程（警告和错误报告、调试，甚至程序分析）时，程序翻译并不比美化的宏语言更强大。在本文中，我们提出了一种增强的方法，语言扩展的Prolog，符号注释包括在目标程序。这些注释允许有选择地反转翻译的代码。我们说明了这种方法，通过显示，耦合它与最小的扩展到一个通用的Prolog调试器，使我们能够为用户提供一个熟悉的，源代码级的视图，在调试过程中使用的各种语言扩展，如功能符号，DCG，或CLP{Q，R}的程序。
2013-01-31 cs.PL
An overview of Ciao and its design philosophy
我们提供了一个全面的描述Ciao多范式编程系统，强调其设计和实现背后的一些新的方面和动机。Ciao的一个重要方面是，除了支持逻辑编程（特别是Prolog）之外，它还为程序员提供了大量来自不同编程范式和风格的有用功能，并且每个程序模块都可以随意打开和关闭这些功能（包括Prolog的功能）。因此，给定模块可以使用例如，高阶函数和约束，而另一个模块可能使用赋值、谓词、Prolog元编程和并发。此外，该语言被设计为以简单和模块化的方式进行扩展。Ciao的另一个重要方面是它的编程环境，它提供了一个强大的预处理器（带有相关的断言语言），能够静态地发现非平凡的bug，验证程序是否符合规范，并执行许多类型的优化（包括自动并行化）。此类优化产生的代码与其他动态语言或（实验性）优化编译器甚至静态语言具有高度竞争力，同时保留动态语言的灵活性和交互式开发。这种编译体系结构支持模块化和独立编译。该环境还包括一个功能强大的自动文档管理器和一个单元测试框架，两者都与断言系统紧密集成。本文提供了语言和程序开发环境的非正式概述。它旨在说明设计哲学，而不是详尽无遗，这在一篇期刊论文中是不可能的，而是指向以前的Ciao文献。
2011-02-27 cs.PL
Casting of the WAM as an EAM
逻辑编程提供了一个非常高级的编程视图，这是以牺牲一些执行效率为代价的。因此，提高逻辑程序的性能是Prolog系统实现的圣杯之一，历史上已经采取了各种各样的方法来实现这一目标。设计既利用给定应用程序中的可用并行性又努力减少所探索的搜索空间的计算模型是多年来一直在进行的研究。特别是这些目标促使设计了几个计算模型，其中之一是安道尔扩展模型。在本文中，我们提出了一个初步的规范和实现的EAM与隐式控制，WAM2EAM，它提供了定期WAM指令与EAM为中心的解释。
2010-09-20 cs.PL
Building a Secure Software Supply Chain with GNU Guix
软件供应链正在成为一个广泛的类比，以指定从开发人员发布的源代码到用户运行的可执行程序所采取的一系列步骤。电脑这些步骤中的任何一个安全漏洞都会使用户面临风险，有证据表明，对供应链的攻击变得越来越普遍。在一个依赖于许多相互关联的软件系统的社会中，对软件供应链的攻击可能会造成悲惨的后果，这导致了对供应链安全的研究兴趣和政府激励措施的增加。GNU Guix是一个软件部署工具和软件发行版，支持出处跟踪、可复制的构建和可复制的软件环境。与许多软件发行版不同，它完全由源代码组成：它提供了一组描述如何从源代码构建代码的包定义。这些属性使它与许多以分发二进制文件为中心的部署工具区别开来。本文主要讨论一个研究问题：Guix和类似的系统如何允许用户安全地更新他们的软件？Guix源代码使用Git版本控制系统分发;更新Guix安装的软件包意味着首先更新Guix源代码的本地副本。以前关于安全软件更新的工作主要集中在与Guix非常不同的系统上--如Debian、Fedora或PyPI，其中更新包括获取有关最新二进制工件的元数据--并且在Guix的上下文中基本上不适用。相比之下，Guix的主要威胁是对其源代码存储库的攻击，这可能导致用户运行不真实的代码或降级他们的系统。从Nix到Portage，与Guix更相似的部署工具要么缺乏安全的更新机制，要么存在缺陷。我们的主要贡献是一个模型和工具来验证新的Git版本。我们…
2022-06-28 cs.PL cs.SE
