Toward Semantic Foundations for Program Editors
程序设计语言定义为完整的程序赋予形式意义。然而，程序员花了大量的时间与不完整的程序进行交互-有漏洞，类型不一致和绑定不一致的程序-使用程序编辑器和实时编程环境（交织编辑和评估）等工具。语义学家在形式化描述（1）不完整程序的静态和动态语义，（2）程序员在编辑和检查不完整程序时可以采取的行动，以及（3）基于从正在编辑的不完整程序中提取的语义信息向程序员建议可能的编辑动作的编辑器服务的行为，以及系统过去遇到的程序。因此，每个工具设计者在很大程度上都被留下来开发自己的特殊工具。本文作为一个研究计划，旨在发展这些“失踪”的语义基础的愿景声明。我们的希望是，这些贡献，这将采取一系列简单的形式演算配备了一个易于处理的元理论，将指导各种当前和未来的交互式编程工具的设计，就像各种lambda演算引导现代语言的设计。我们自己的研究将在Hazel的设计中应用这些原则，Hazel是一个实验性的实时实验室笔记本编程环境，专为数据科学任务而设计。我们计划共同设计Hazel语言和编辑器，这样我们就可以探索诸如编辑时语义冲突解决机制和允许库提供商安装特定于库的编辑器服务的机制等概念。
2017-03-25 cs.PL
Conditioning in Probabilistic Programming
我们调查的语义复杂性的条件，概率规划的一个主要特点。我们提供了一个最弱的（自由）前置条件（w（l）p）的基本概率程序设计语言pGCL扩展条件的语义。我们证明了定量最弱（自由）的先决条件与条件（自由）期望回报的马尔可夫链，并表明语义条件是一个真正的保守扩展。我们提出了两个程序转换，完全消除任何程序的条件，并证明其正确性使用的w（l）p-语义。最后，我们展示了如何的w（l）p-语义可以用来确定条件概率的参数匿名协议，并表明，一个归纳的w（l）p-语义的条件在非确定性的概率程序不存在。
2015-04-01 cs.PL
Distribution Theoretic Semantics for Non-Smooth Differentiable Programming
随着深度学习和受梯度下降启发的优化算法的广泛传播，可微编程获得了关注。如今，它已经在许多不同的领域，如科学计算，机器人，计算机图形学和其他应用。它的一个众所周知的困难问题在于解释不是处处可微的程序。在这项工作中，我们定义了$λ_δ$，一个核心演算的非光滑可微程序，并定义其语义使用的概念分布理论，一个完善的功能分析领域。我们还展示了如何$λ_δ$提出了更好的方程比其他现有的语义属性，并使用我们的语义的原因简化的光线追踪算法。此外，我们与我们的语义现有的微分语言提供翻译和其他现有的微分语义模型。最后，我们在PyTorch中提供了本文中新颖结构的概念验证实现。
2022-07-13 cs.PL
LAGC Semantics of Concurrent Programming Languages
形式化的、数学上严格的程序设计语言语义是设计允许对并发程序进行自动推理的逻辑和演算的基本先决条件。我们提出了一种新的模块化语义，旨在顺利对齐与演绎验证和并发程序的形式规范中使用的程序逻辑。我们的语义分离的表达式和语句的本地评估在一个抽象的，符号化的环境，从他们的组合成全球性的计算，在这一点上，他们是具体化。这使得可以逐步增加新的语言概念，而不需要修改框架。的基础是一个概括的概念，一个程序跟踪作为一个序列的不断发展的状态，我们丰富的事件描述符和尾随延续标记。这允许将调度约束从局部评估的级别推迟到全局组合阶段，其中在事件结构上的格式良好性谓词声明性地描述了广泛的并发模型。我们还说明了如何一个健全的程序逻辑和演算可以定义这种语义。
2022-02-24 cs.PL
Coalgebraic Logic Programming: from Semantics to Implementation
共归纳定义，例如无限流的定义，通常可以用优雅的逻辑程序来描述，但是对于那些SLD-反驳没有价值的定义，因为SLD-推导会陷入无限循环。这样的定义引起了惰性共递归推导和并行性的问题，因为这样的逻辑程序的执行可以同时具有递归和共递归特性。观察语义学和共代数语义学已经被用来抽象地研究它们。方案拟订工作往往是单独进行的，而且通常是以执行为主导的。在这里，我们给出了一个连贯的语义为主导的帐户的问题，从抽象的范畴理论语义，发展coalgebra，自然产生的树，并着手实现一个新的方言，CoALP，逻辑编程，其特点是由看守懒惰corecursion和并行。
2013-12-23 cs.PL
A Semantics for Approximate Program Transformations
近似程序转换是一种可以在指定的经验误差范围内改变程序语义的转换。这种转换有广泛的应用：它们可以减少计算时间，功耗和内存使用，并且在某些情况下，可以允许实现不可计算的操作。近似程序变换的正确性证明是定量的。不幸的是，与标准程序转换不同，目前还没有模块化的方法来证明近似转换本身的正确性。误差界必须证明每个转换程序单独，并必须重新证明每次修改程序或一组不同的近似应用。在本文中，我们给出了一个语义，使定量推理的一个大类的近似程序变换的本地，组合的方式。我们的语义是基于程序之间的距离的概念，它定义了一个近似变换是正确的错误界意味着什么。关键的见解是，程序之间的距离一般不能用度量空间和实数来表示。相反，我们的语义承认每个类型构造的距离的自然概念;例如，数字被用作数值数据的距离，函数被用作函数数据的距离，多态数据项被用作多态数据的距离。然后，我们将展示我们的语义如何应用于两个示例近似：用浮点数替换实数和循环穿孔。
2013-04-19 cs.PL
A Pure Demand Operational Semantics with Applications to Program Analysis
本文提出一种仅依赖调用栈和词法层级的高阶函数式语言最小状态操作语义，证明其与标准语义等价，并基于其直接有限化构建了可推导递推、无需值拓宽的新型程序分析，给出了形式化定义与实现。
2024-03-07 cs.PL
Compositional Semantics for the Procedural Interpretation of Logic
逻辑程序的语义由证明论、模型论和直接后果算子的不动点给出。如果子句逻辑是一种程序设计语言，那么它也应该具有组合语义。程序设计语言的组合语义遵循程序的抽象语法，通过对其组成单元的含义进行数学运算来组成单元的含义。逻辑的过程解释只产生了逻辑程序的不完整的抽象语法。我们完成它，并使用的结果作为基础的组合语义。我们提出比较塔斯基的代数化的一阶谓词逻辑，这是在实质上的组合语义为他选择的语法。我们的特点是我们的语义等价的直接后果运营商。
2006-05-07 cs.PL
π: Towards a Simple Formal Semantic Framework for Compiler Construction
本文提出了一种用于编译器构造和程序验证的形式化语义框架π。π由π Lib和π Automata组成，π Lib是一组受Peter Mosses的基于语义的程序设计语言构造启发的构造，π Automata是一种基于自动机的形式主义，用于描述程序设计语言的操作语义，它概括了Gordon Plotkin的解释自动机。
2018-07-31 cs.PL
Mechanized semantics
本讲座的目标是展示现代定理证明器--在本例中，Coq证明助手--如何用于机械化程序设计语言及其语义的规范，以及如何对单个程序和通用程序转换进行推理，如通常在编译器中发现的那样。所涵盖的主题包括：操作语义学（小步、大步、定义解释器）;指称语义的简单形式;公理语义学和霍尔逻辑;验证条件的生成，以及对程序证明的应用;编译成虚拟机器码及其正确性证明;优化程序转换（死代码消除）及其正确性证明的示例。
2010-10-27 cs.PL
An Effective Fixpoint Semantics for Linear Logic Programs
在本文中，我们调查的理论基础，一个新的自下而上的语义线性逻辑程序，更确切地说，为片段的LinLog，包括语言LO丰富的常数1。我们使用约束来象征性地和非象征性地表示可能无限的可证明目标的集合。我们基于TP处理约束风格的新运算符定义了不动点语义。不动点算子的应用可以通过算法来计算。作为终止的充分条件，我们证明了不动点计算是保证收敛命题LO。据我们所知，这是首次尝试为线性逻辑程序定义有效的不动点语义。作为我们的框架的应用，我们还提出了一个正式的调查LO和析取逻辑编程之间的关系。使用一种基于抽象解释的方法，我们表明，DLP不动点语义可以被视为我们的语义LO的抽象。我们证明，由此产生的抽象是正确的和完整的一个有趣的类LO程序编码Petri网。
2001-03-23 cs.PL
Semantics of Sets of Programs
本文提出程序集合的最小组合指称语义，揭示跟踪无界多次执行中的不同行为是验证的充要条件，并导出首个可靠且相对完备的 Hoare 风格逻辑。
2025-07-27 cs.PL
ChopChop: a Programmable Framework for Semantically Constraining the Output of Language Models
University of California San Diego（加州大学圣迭戈分校）
ChopChop是一种可编程框架，通过语义约束提升语言模型输出的正确性和类型安全性。
2025-12-02 cs.PL
Density-Based Semantics for Reactive Probabilistic Programming
针对概率同步语言仅对已调度方程定义语义的局限，提出两种与调度无关的基于密度函数流的语义（共迭代与关系语义），并利用关系语义证明了状态空间模型优化推理所需程序变换的正确性。
2023-09-07 cs.PL
A Thread-Local Semantics and Efficient Static Analyses for Race Free Programs
无数据竞争程序是一类重要的并发程序。在本文中，我们提供了一个框架，设计和证明的正确性数据流分析，针对这一类的程序。这些分析与早期文献中提出的“同步-CFG”分析具有相同的精神。为了实现这一点，我们首先提出了一种新的具体语义DRF程序，称为L-DRF，这是线程本地的性质-每个线程操作自己的副本的数据状态。我们表明，我们的语义抽象，使我们能够减少DRF程序的分析，顺序分析。这有助于将现有的顺序分析快速移植到DRF程序的合理和可扩展的分析中。接下来，我们将L-DRF参数化，将程序变量划分为原子访问的“区域”。区域参数化语义的抽象产生更精确的分析“区域种族”自由并发程序。我们实例化这些抽象设计高效的关系分析种族自由的程序，我们已经实现了一个原型工具，称为RATCOP。在基准测试中，RATCOP能够证明高达65%的断言，相比之下，我们的基线证明了25%。此外，在与最近的并发静态分析器的比较研究中，RATCOP快了5个数量级。
2020-09-06 cs.PL
Reasoning about Iteration and Recursion Uniformly based on Big-step Semantics
可靠的演绎程序验证技术应该被证明是相对于程序设计语言的语义合理的。对于每一种不同的语言，构造一个单独的可靠性证明往往是一项艰巨的任务。在独立于语言的程序验证中，讨论了计算机程序的共同方面，以使所有语言都能进行合理的推理。在这项工作中，我们提出了一个解决方案，合理的推理迭代和递归的基础上的大步骤操作语义的任何程序设计语言。我们给出了我们的推理技术的合理性和相对完整性的归纳证明。我们说明了在简化的程序设计语言的命令式和功能的范例，具有不同的功能的技术。我们还在Coq证明助手中机制化所有正式结果。
2021-08-04 cs.PL
Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with Monotonic Semantics
本文提出在通用SemGuS框架下，利用语言语义的单调性属性，自动从具体语义获取基于区间的抽象语义以实现自动化剪枝，无需手动设计抽象域，有效提升了程序综合的搜索效率。
2024-08-28 cs.PL
An Application of Computable Distributions to the Semantics of Probabilistic Programs
在本章中，我们将探讨如何使用（第2类）可计算分布来为具有连续分布的概率程序提供（算法）采样和分布语义。为此，我们勾勒出一个编码的可计算分布在一个片段的Haskell和拓扑域可以用来模拟所产生的PCF类语言。我们还研究的影响，（类型-2）可计算语义实现条件反射。我们希望在整个章节中找出基于（第二类）可计算性的方法与普通编程之间的联系，并强调与构造性数学（通过可实现性）的关系。
2019-07-30 cs.PL
When Do Staging Annotations Preserve Semantics? Mechanizing Typed Semantics-Preserving Multi-stage Programming with Let-Insertion (Extended Version)
Tufts University（塔夫茨大学）
研究带引用的多阶段编程中阶段注释保持语义的条件，提出两个带类型的两阶段演算，通过自动let插入和轻量类型-效应系统实现语义保持，并证明强语义保持定理。
2026-08-24 cs.PL
Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic Programs
我们定义了一个新的，可拓的，三值语义的高阶逻辑程序与否定。新的语义是基于解释类型的源语言作为三值拟合单调函数在所有级别的类型层次结构。我们证明了这样的拟合单调函数和双值结果函数对之间存在一个双射，其中该对的第一个成员是单调-反单调的，第二个成员是反单调-单调的。通过推导一致近似不动点理论（Denecker et al. 2004）的扩展并利用上述双射，我们定义了一个迭代过程，该过程为任何给定的高阶逻辑程序产生一个杰出的扩展模型。我们证明，这个模型实际上是一个最小的。此外，我们证明，我们的建设推广了熟悉的良好的基础语义的经典逻辑程序，使我们的建议，以这种方式一个有吸引力的制定捕捉良好的基础语义高阶逻辑程序。本文件正在考虑被TPLP接受。
2018-04-23 cs.PL
Verifying Semantic Conflict-Freedom in Three-Way Program Merges
尽管许多程序员依赖于三向合并工具来集成来自不同分支的更改，但此类工具可能会在集成过程中引入细微的错误。本文旨在通过定义冲突自由的语义概念来缓解这个问题，这确保了合并后的程序不会引入新的不必要的行为。我们还展示了如何使用一种新颖的组合算法来验证此属性，该算法结合了对共享程序片段的轻量级依赖分析和对修改的精确关系推理。我们评估了我们的工具SafeMerge从Github获得的52个真实世界的合并场景，并将结果与文本合并工具进行比较。实验结果表明，我们的方法的好处，语法冲突自由，并表明SafeMerge是精确和实用的。
2018-02-19 cs.PL
A Three-Valued Semantics for Typed Logic Programming
逻辑编程中的类型一方面关注常规类型对程序语义的保守近似，另一方面关注基于为类型化程序定义的规定语义的类型系统。在本文中，我们定义了一个新的语义逻辑编程，程序评估为真，假，并称为错误的一个新的语义值，对应于一个运行时类型错误。这样我们就有了一种具有分离的类型语义的类型语言。最后，我们定义了一个类型系统的逻辑编程，并证明它是语义上的声音相对于程序和类型之间的语义关系，如果一个程序有一个类型，那么它的语义是没有错的。我们的工作遵循米尔纳的方法类型的函数语言的语义程序是独立的类型的语义，类型系统被证明是健全的两个语义之间的关系。
2019-09-18 cs.LO cs.PL
Presynthesis: Towards Scaling Up Program Synthesis with Finer-Grained Abstract Semantics
University of Michigan（密歇根大学）；University of Texas at Austin（德克萨斯大学奥斯汀分校）
本文提出Presynthesis方法，通过引入离线预合成阶段，利用树自动机和oracle提升程序合成效率，显著优于现有方法。
2026-04-16 cs.PL
Mechanization of LAGC Semantics in Isabelle
当试图以自动方式验证程序的属性时，形式化的程序设计语言语义是必不可少的。Din等人使用一种新的方法，通过提出一种模块化的跟踪语义来加强对并发程序的推理能力，该语义可以灵活地适应最突出的命令式程序设计语言范例。这些语义通过为个体的局部系统生成抽象的、符号化的轨迹，将局部环境中的评价与全局环境中的评价解耦。然后，这些轨迹被组合和具体化，从而产生全局系统的全局轨迹。因此，这些语义被称为局部抽象，全局具体（LAGC）。在这项工作中，我们提出了一个形式化的LAGC语义流行的定理证明环境Isabelle/HOL。给出的模型是基于Din等人先前关于LAGC语义理论的工作，包括基本定理的形式化、While语言（WL）的LAGC语义以及While语言的扩展版本（WLEXT）的LAGC语义。此外，我们使用我们的伊莎贝尔模型，以提供正式的证明LAGC语义，这还没有在原来的文件中分析的几个先进的性能。虽然工作的主要目标是以数学上严格的方式形式化LAGC语义，但我们也实现了高水平的证明自动化，并设法为程序痕迹的计算提供高效的代码生成。由于语义的形式化是高度模块化的，所给出的理论在将来可以扩展到更复杂的程序设计语言范例。
2022-02-16 cs.PL
Singular and Plural Functions for Functional Logic Programming
函数逻辑编程（FLP）语言使用非终止和非汇合构造器系统（CS）作为程序，以便定义非严格非确定性函数。对于这类函数的参数传递，通常考虑两种语义选择：调用时选择和运行时选择。虽然前者是现代FLP语言的标准选择，但后者缺乏一些属性--主要是组合性--这阻碍了它在实际FLP系统中的使用。传统上，它已被认为是调用时的选择诱导一个单一的指称语义，而运行时的选择诱导一个复数的语义。我们已经发现，后者的识别是错误的，当涉及到模式匹配，因此，我们提出了两个新的组合复数语义CS的是不同的运行时的选择。我们研究了我们的复数语义的基本属性-组合性，极性，单调性的替代，和构造函数系统的冒泡属性的限制形式-以及它们之间的关系和以前的建议，得出的结论是，这些语义形成了一个层次结构的意义上的集合包含的一组计算值。我们还确定了一类程序，其特征在于所提出的复数语义的行为相同的语法标准，和一个程序转换，可以用来模拟其中之一的长期重写。在实践层面上，我们研究如何使用这些语义的表达能力，以提高程序的声明味。我们还提出了一种语言，结合调用时间的选择和我们的复数语义，我们已经实现了在莫德。由此产生的解释器被用来测试几个显着的例子显示的组合语义的能力。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
2012-03-12 cs.PL
The Parallel Semantics Program Dependence Graph
针对现有并行IR缺少语义等价约束捕获表示、顺序PDG不适用于并行代码的问题，提出并行语义程序依赖图PS-PDG，论证其扩展必要性并验证其优化能力更强，助力编译器在保语义下选择并行执行计划。
2024-02-01 cs.PL
Relating Weight Constraint and Aggregate Programs: Semantics and Representation
权约束和聚集程序是最广泛使用的带约束的逻辑程序。在本文中，我们涉及这两类程序的语义，即稳定的模型语义的权重约束程序和答案集语义的基础上的条件满足聚合程序。这两类程序都是具有约束的逻辑程序的实例，并且特别地，聚合程序的答案集语义可以应用于权重约束程序。我们表明，这两个语义是密切相关的。首先，我们表明，广泛的一类重量约束的程序，称为强可满足的程序，这两个语义一致。当它们不一致时，由稳定模型语义承认的稳定模型可以循环地证明。我们表明，这两种语义之间的差距可以通过将权重约束程序转换为强可满足的程序来关闭，因此在当前实现的稳定模型语义下可能不会生成循环模型。我们进一步证明了这两个语义之间的密切关系，制定一个转换从权重约束程序到逻辑程序与嵌套表达式，保留了答案集语义。我们的语义研究导致了一个方法论问题的调查，即可能性的紧凑表示的聚合程序的重量约束程序。我们表明，几乎所有的标准聚集可以编码的重量约束competencies。这使得有可能计算的答案集的聚合程序使用的ASP求解器的重量约束的程序。这种方法进行了实验比较，其中聚集处理更明确，这表明，权重约束编码的聚集，使一个有竞争力的方法来回答集计算的聚集程序。
2011-05-16 cs.LO cs.PL
Semantically Reflected Programs
IT University of Copenhagen（哥本哈根信息技术大学）；University of Oslo（奥斯陆大学）
本文通过语义提升程序解决结构化与行为化知识形式化之间的矛盾，提出面向对象编程语言的语义反射层，通过地质建模案例展示其应用。
2026-04-07 cs.LO cs.PL
The Semantics of Graph Programs
GP（图形程序）是一种基于规则的、非确定性的程序设计语言，用于在高抽象级别上解决图形问题，使程序员从处理低级别的数据结构中解放出来。GP的核心由四个结构组成：一组条件图转换规则的单步应用，顺序组合，分支和迭代。我们提出了一个形式化的语义GP的结构操作语义的风格。我们的语义的一个特殊功能是使用失败的程序来定义GP的强大的分支和迭代命令。
2010-03-24 cs.LO cs.PL
Program Synthesis and Linear Operator Semantics
对于确定性和概率性的程序，我们调查的问题，程序合成和程序优化（相对于非功能属性）的一般设置的全局优化。这种方法是基于表示的语义的程序和程序片段的线性运算符，即矩阵。我们特别利用的事实，我们可以自动生成的基本块的语义表示。然后可以使用这些来组合整个程序的语义，即相应的离散时间马尔可夫链（DTMC）的生成器。我们还利用一个广义版本的抽象解释适合这个线性代数或功能分析框架，以制定语义约束（不变量）和优化目标（例如性能要求）。
2014-07-21 cs.PF cs.PL
Learning Scalable and Precise Representation of Program Semantics
Visa Research（Visa研究院）
神经程序嵌入已显示出帮助分析大规模复杂软件的潜力。新提出的深度神经架构以学习程序语义而不是表面的语法特征为荣。然而，由于只考虑源代码，绝大多数神经网络不能捕获程序语义的深层精确表示。在本文中，我们提出了\dypro，一种新的深度神经网络，从程序执行轨迹学习。与现有的动态模型相比，\dypro不仅能够在多个执行中泛化，以整体地学习程序的动态语义，而且\dypro在处理产生长执行轨迹的程序时也更有效。为了进行评估，我们对\dypro进行了语义分类（即根据语义对程序进行分类），并将其与两个主要的静态模型进行了比较：门控图神经网络和TreeLSTM。我们发现，\dypro达到所有模型中最高的预测精度。为了进一步揭示所有上述深度神经架构的能力，我们研究了模型是否可以学习检测程序的更深层次语义属性。特别是考虑到识别循环不变的任务，我们显示\dypro击败了所有静态模型的一个很大的利润。
2019-05-26 cs.LG cs.PL
Towards the Future: Bring Program Correctness back to the focus
在形式语义是一个热门话题的早期，程序正确性曾经是计算机软件的主要关注点。但是，“正确”一词后来被可靠、稳健和值得信赖等取代，一个折衷的情况。这并不是因为正确性不再重要，而是因为人们发现没有办法在这个方向上取得成功。这种权衡导致软件工程师专注于技术和测试工具。软件工程的快速发展现在已经达到了一个高峰，程序员现在可以自由地工作，而不用太担心bug，因为bug是无法避免的。今天讨论程序正确性有意义吗？我们的答案是肯定的。现在是再次认真考虑正确性的时候了，在为时已晚之前，为未来做好准备。下一代计算机系统在语法（静态）和语义（动态）上都应该是正确的。第一作者的《OESPA：面向语义的编程理论》（2019）一书为语义研究开辟了新的方向。从理论上讲，基于OESPA，可以从程序文本中计算出程序语义，从而证明程序的正确性。但是，当程序规模较大时，语义计算和正确性证明无法手工完成。自动工具是必要的。本文的工作为开发所需的自动化工具奠定了基础，从而丰富了OESPA，使之更好地服务于未来的需要。为此，提出了条件语义谓词的概念。对OESPA中的语义函数、语义谓词、语义公式和语义演算等概念进行了重新表示。这种重新介绍是必要的，因为这本书是唯一的出版物语义演算迄今为止。新版本的语义演算说明了如何进行语义自动计算。
2022-03-29 cs.PL cs.SE
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
Equivalence of two Fixed-Point Semantics for Definitional Higher-Order Logic Programs
已经提出了两种不同的研究方法分配一个纯粹的扩展语义高阶逻辑编程。前一种方法使用经典的域理论工具，而后者建立在一个固定的点构造上定义的语法实例的源程序。这两种方法之间的关系尚未被调查，直到现在。在本文中，我们证明了对于一类非常广泛的程序，即由W。W. Wadge，这两种方法是一致的（相对于涉及程序符号的基础原子）。另一方面，我们认为，如果存在的高阶变量被允许出现在身体的程序规则，这两种方法是在一般不同的。本文的结果有助于更好地理解高阶逻辑编程的语义。
2015-09-10 cs.LO cs.PL
Semantics of higher-order probabilistic programs with conditioning
University College London（伦敦大学学院）；Cornell University（康奈尔大学）
我们提出了一个指称语义高阶概率规划的线性算子之间的Banach空间。我们的语义是植根于经典理论的Banach空间及其张量积，但承担的相似之处与著名的斯科特语义的高阶程序通过使用有序的Banach空间，允许定义的不动点。基于一个monoidal而不是carnival封闭结构，我们的语义有效地把随机性作为一种资源。
2019-02-28 cs.LG cs.LO cs.PL
Giving Semantics to Program-Counter Labels via Secure Effects
为信息流控制而设计的类型系统通常使用程序计数器标签来跟踪上下文的敏感性，并排除敏感上下文中有效计算所引起的数据泄漏。目前，除了在安全证明中，类型系统设计者使用特别的技术，他们非正式地推理这个标签。我们开发了一个框架的基础上一元语义的影响，语义程序计数器标签。这个框架导致了三个结果的程序计数器标签。首先，我们开发了一种新的证明技术，用于有效语言中的信息流控制的核心安全定理。其次，我们统一了不同类型的效果，包括国家，例外和非终止的安全概念。最后，我们正式的民间传说，程序计数器标签是一个下界的影响。我们表明，虽然不是普遍正确的，这个民间传说有一个良好的语义基础。
2020-12-10 cs.CR cs.PL
Denotational Semantics for Probabilistic and Concurrent Programs
本文针对兼具概率动作与并行组合的命令式程序，提出具有良好域论性质的指称模型，并通过两个适当性定理证明其统一涵盖并发与概率非确定语义。
2025-06-07 cs.LO cs.PL
Predicting Program Exit Code with LLMs and Programming Language Semantics
The University of Texas at Austin（德克萨斯大学奥斯汀分校）；Cisco Research（思科研究院）
本研究提出程序可执行性预测（PrEx）任务，构建含系统生成非法变换的数据集，评估开源编码LLM，发现其依赖预训练先验而非给定语义，在修改语义及复杂程序上表现差。
2026-09-02 cs.AI cs.CL cs.PL
Relaxed Operational Semantics of Concurrent Programming Languages
我们提出了一种新颖的，可操作的框架，正式描述的语义并发程序运行在一个宽松的内存模型的上下文中。我们的框架具有一个“临时存储”的内存操作发出的线程记录，在程序顺序。然后，内存模型指定允许全局执行此序列中的挂起操作的条件，可能是无序的。内存模型还涉及“写粒度”，这说明了线程可能读取尚未全局可见的写操作的架构。我们的正式模型是由一个软件模拟器支持，使我们能够在我们的语义运行石蕊测试。
2012-08-14 cs.LO cs.PL
Software Language Comprehension using a Program-Derived Semantics Graph
University of California, Los Angeles（加利福尼亚大学洛杉矶分校）；Intel Labs（英特尔实验室）；University of Pennsylvania（宾夕法尼亚大学）
传统的代码转换结构，例如抽象语法树（AST）、抽象流图（XFG），以及更一般地，编译器中间表示（IR），在从代码中提取高阶语义方面可能具有限制。虽然高阶语义提升的工作已经开始（例如，Aroma的简化解析树（SPT）、验证提升的lambda演算和Halide的意向领域特定语言（DSL）），这方面的研究还不成熟。为了继续推进这项研究，我们提出了程序派生的语义图，一个新的图形结构来捕捉代码的语义。PSG的目的是提供一个单一的结构捕捉程序语义在多个层次的抽象。PSG可能属于一类新兴的结构化表示，这些结构化表示不能从传统的一组预定义规则构建，而是必须学习。在本文中，我们描述了PSG和它的基本结构差异相比，国家的最先进的结构。虽然我们对程序语义图的研究还处于起步阶段，但我们的初步结果和体系结构分析表明，自动提取程序语义是一个很有前途的新研究方向。
2020-12-11 cs.AI cs.PL
SEMBridge: Tagless-Final Program Semantics with Weakest-Precondition and Bounded-Checking Interpretations
Oracle
提出SEMBridge框架，通过无标签最终风格统一生成可执行语义、最弱前置条件验证条件和有界检查，保持三者同步。
2026-05-29 cs.AI cs.PL
Logic Programming Semantics for Causal Processes
German University Of Digital Science Potsdam（德国波茨坦数字科学大学）
研究逻辑程序设计语义与因果过程最终状态的关系，指出正逻辑程序稳定模型对应特定过程最终状态，支持模型描述任意起点可达状态，为逻辑程序设计语义讨论提供新视角及时间维度。
2026-07-24 cs.AI cs.LO cs.PL
Dynamic Neural Program Embedding for Program Repair
University of California（加利福尼亚大学）；Microsoft Research（微软研究院）
神经程序嵌入已经显示出了很大的希望，最近的各种程序分析任务，包括程序合成，程序修复，故障定位等，然而，大多数现有的程序嵌入是基于程序的语法特征，如原始令牌序列或抽象语法树。与图像和文本不同，程序具有明确的语义含义，仅考虑其语法可能难以捕获（即，语法相似的程序可能表现出截然不同的运行时行为），这使得基于语法的程序嵌入从根本上受到限制。本文提出了一种新颖的语义程序嵌入，它是从程序执行轨迹中学习的。我们的关键见解是，表示为实时变量值的顺序元组的程序状态不仅更精确地捕获程序语义，而且还为递归神经网络建模提供了更自然的拟合。我们评估不同的语法和语义程序嵌入预测的错误类型，学生在提交给一个入门编程类和两个练习CodeHunt教育平台。评估结果表明，我们的新的语义程序嵌入显着优于基于令牌序列和抽象语法树的语法程序嵌入。此外，我们增加了基于搜索的程序修复系统，从我们的se-mantic嵌入获得的预测，并显示搜索效率也显着提高。
2018-06-30 cs.AI cs.PL
Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies (Extended Version)
近年来，随着操作语义和相关逻辑的发展，C11程序的演绎验证技术有了很大的进步。然而，这些语义和逻辑是在受限的环境中开发的，以避免稀薄空气读取问题。在本文中，我们提出了一个操作语义，利用线程内的偏序（称为语义依赖）诱导最近开发的指称事件结构为基础的语义。我们证明了我们的操作语义是健全的和完整的指称语义。我们提出了一个相关的逻辑，概括了最近Owicki-Gries框架RC 11（修复C11），并证明了使用这种逻辑的几个例子证明。
2021-08-03 cs.LO cs.PL
Evaluation of Generalizability of Neural Program Analyzers under Semantic-Preserving Transformations
University of Houston（休斯顿大学）
丰富的公开源代码库，结合神经网络的进步，使数据驱动的方法程序分析成为可能。这些方法称为神经程序分析器，使用神经网络来提取程序中的模式，用于从开发生产力到程序推理的任务。尽管神经程序分析器越来越受欢迎，但其结果的可推广程度尚不清楚。在本文中，我们使用七个语义等价的程序变换对两个流行的神经程序分析器的泛化能力进行了大规模的评估。我们的研究结果警告说，在许多情况下，神经程序分析器不能很好地概括，有时程序的文本差异可以忽略不计。这些结果为神经程序分析器中的鲁棒性量化提供了初步的基础。
2021-03-18 cs.LG cs.PL cs.SE
Hybrid Semantics of Stochastic Programs with Dynamic Reconfiguration
我们首先回顾了一种技术来近似随机程序的动态-写在随机过程代数-由一个混合系统，适合捕捉混合离散/连续演化。简而言之，离散动态保持随机，而连续演化以常微分方程给出，因此，整体技术自然地将分段确定性马尔可夫过程与随机程序相关联。在这项工作中的具体贡献包括在增加的灵活性的翻译计划，通过允许动态重新配置的程度的离散性/连续性的语义。我们还讨论了这种方法与其他生化系统的混合仿真策略的关系。
2009-10-08 cs.LO cs.PL
Operational methods in semantics
本文以编程语言操作语义为核心，从抽象计算步骤出发构建语义等价、规范语言与静态分析，展示了该方法在语言实现与程序验证中的有效性与可扩展性。
2025-10-14 cs.LO cs.PL
Representing Partial Programs with Blended Abstract Semantics
Massachusetts Institute of Technology（麻省理工学院）
从例子中合成程序需要在可能的程序的巨大的组合空间中搜索。在这个搜索过程中，一个关键的挑战是在程序可以执行之前表示部分编写的程序的行为，以判断它是否在正确的轨道上，并预测下一步在哪里搜索。我们介绍了一种通用的技术，用于表示部分编写的程序中的程序合成引擎。我们从抽象解释的技术，其中一个近似的执行模型是用来确定一个未完成的程序将最终满足一个目标规范的灵感。在这里，我们学习了一个近似的执行模型，它被实现为一个模块化的神经网络。通过构建组合程序表示，隐式编码的解释语义的底层程序设计语言，我们可以表示部分程序使用一个灵活的组合，具体的执行状态和学习的神经表示，使用学习的近似语义时，具体的语义是未知的（在未完成的部分程序）。我们表明，这些混合神经符号表示，使执行指导的合成器使用更强大的语言结构，如循环和高阶函数，并可以用来合成程序更准确地为一个给定的搜索预算比纯神经方法在几个领域。
2021-04-19 cs.AI cs.LG cs.PL
Semantics and Termination of Simply-Moded Logic Programs with Dynamic Scheduling
在逻辑编程中，动态调度是指在运行时确定每个解析（计算）步骤中原子的选择的情况，而不是像Prolog中从左到右的选择规则。这在例如并行编程中具有应用。在现有的语言中，以延迟声明的形式提供了一种控制动态调度的机制。在抽象技术细节的同时，引入了消耗输入的推导来描述动态调度。在本文中，我们首先正式延迟声明和输入消费派生之间的关系，在许多情况下，一对一的对应关系。然后，我们定义了一个模型理论的语义输入消费派生的简单模式的程序。最后，对于这类程序，我们提供了一个终止的充分必要条件。
2001-01-23 cs.LO cs.PL
Visualization of Constraint Handling Rules: Semantics and Applications
本文提出了一种对约束处理规则的动画扩展（$CHR^{vis}$）。可视化总是帮助程序员理解数据和调试程序。一张图片胜过千言万语。它可以帮助识别问题所在或显示某些东西是如何工作的。它甚至可以说明一个关系，否则是不清楚的。$CHR^{vis}$旨在将动画和可视化功能嵌入到可编程逻辑器件程序中。因此，它使用户能够在执行程序时使这些执行动画化。本文旨在为$CHR^{vis}$提供操作语义。文中还讨论了$CHR^{vis}$程序的正确性。文中还介绍了新扩张的一些应用。
2017-06-04 cs.PL cs.SE
Deductive Verification of Programs with Underspecified Semantics by Model Extraction
本文提出了一种新的、自动化程度高的语义欠规范程序的形式化验证方法，一种语言语义学，它不确定某些求值的顺序。首先，我们减少这个问题的非确定性的分布式系统，自动提取一个分布式的主动对象模型，欠指定的，顺序的C代码。这个翻译过程为所考虑的C子集提供了一个完全正式的语义。在所提取的模型中，每个非确定性选择对应于一个可能的评估顺序。此步骤还自动将ANSI/ISO C规约语言（ACSL）中的规范转换为活动对象的方法契约和对象不变量。然后，我们对指定的Active Objects模型执行验证。为此，我们已经实现了一个定理证明器Crowbar的基础上的行为程序逻辑（BPL），它验证了提取的模型相对于翻译的规范，并确保原始属性的C代码的所有可能的评估订单。通过使用模型提取，我们可以使用标准的工具，而不需要设计一个新的复杂的程序逻辑来处理欠规格说明。所使用的案例研究是高度低估，不能用现有的C语言工具进行验证。
2022-02-11 cs.LO cs.PL
Pretty-big-step-semantics-based Certified Abstract Interpretation (Preliminary version)
我们提出了一种技术，用于从自然语义规范的程序设计语言的语义程序分析。该技术基于一种特殊的语义，称为pretty-big-step语义。我们提出了一个漂亮的大步骤语义的语言与简单的对象称为O 'While，并指定了一系列的仪表的语义，明确了流程的值在程序中。这导致了基于语义的依赖性分析，在核心，例如，污染分析在软件安全中的应用用Coq证明助手实现了形式化。
2013-09-20 cs.LO cs.PL
Proof rules for purely quantum programs
我们应用D'Hondt和Panangelt提出的量子谓词的概念来分析一个纯粹的量子语言片段，它描述了Knill架构中未来量子计算机的量子部分。介绍了该语言片段的指称语义、最弱前提语义和最弱自由前提语义。为了帮助推理涉及量子循环的量子程序，我们将经典概率程序的证明规则扩展到纯量子程序。
2006-03-16 cs.PL quant-ph
Well-Definedness and Efficient Inference for Probabilistic Logic Programming under the Distribution Semantics
University of Ferrara（费拉拉大学）；Universidade Nova de Lisboa（新里斯本大学）
分布语义是逻辑程序设计与概率论相结合的重要途径之一。许多语言遵循这种语义，例如独立选择逻辑、PRISM、pD、带有注释析取的逻辑程序（LPAD）和ProbLog。当程序包含函数符号时，只有当查询的解释集是有限的并且每个解释也是有限的时，分布语义才是定义良好的。良好定义通常要么是明确强加的，要么是通过严格限制允许程序的类别来实现的。在本文中，我们确定了一个更大的类的程序，其中的语义是定义良好的计算查询的概率与一个有效的程序。由于LPAD提供了最一般的语法，我们提出了我们的结果，但我们的结果适用于所有的语言下的分布语义。我们提出的算法“概率推理与制表和答案包容”（PITA），计算概率的查询转换成一个正常的程序，然后应用SLG决议与答案包容。PITA已经在XSB中实现，并在六个域上进行了测试：两个域带有函数符号，四个域没有。与ProbLog，cplint和CVE的执行时间相比，PITA几乎总是能够在更短的时间内解决更大的问题，无论是否有函数符号。
2011-10-04 cs.AI cs.LO cs.PL
