Syntax and semantics of the weak consistency model specification language cat
Jade Alglave, Patrick Cousot, Luc Maranget
我们提供的语法和语义的猫语言，一个特定领域的语言来描述并行/分布式程序的一致性属性。该语言也在1997年实现（http：//diy.inria.fr/doc/js.html）。
We provide the syntax and semantics of the cat language, a domain specific language to describe consistency properties of parallel/distributed programs. The language is implemented in the herd7 too (http://diy.inria.fr/doc/herd.html)l.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
A Model-Driven Parser Generator, from Abstract Syntax Trees to Abstract Syntax Graphs
基于模型的解析器生成器将语言规范与语言处理解耦。模型驱动的方法避免了传统解析器生成器对语言设计者的限制。传统的工具要求所设计的语言语法符合特定解析器生成器（最常见的是LL和LR解析器生成器）所支持的特定类型的语法。模型驱动的解析器生成器，如ModelCC，不需要语法规范，因为语法可以自动从语言模型中导出，并且如果需要，可以进行调整以符合给定类型解析器的要求，所有这些都不会干扰语言及其相关应用程序的概念设计。此外，模型驱动工具（如ModelCC）能够自动解析语言元素之间的引用，因此作为解析过程的结果，生成抽象语法图而不是抽象语法树。这样的图并不局限于有向无环图，它们可以包含循环，因为ModelCC支持前指、后指和递归引用。
Treo: Textual Syntax for Reo Connectors
Reo是一个以交互为中心的并发模型，用于通信和协调协议的组合规范。存在形式化验证工具以确保Reo中指定的协议的正确性和合规性，其可以容易地在不同的应用程序中（重新）使用，或组成更复杂的协议。最近的基准测试表明，编译这样的高级Reo规范产生的可执行代码可以与使用传统并发结构的C或Java等语言编写的手工程序的性能竞争，甚至击败它们。Reo的原始声明性图形语法不支持参数传递、迭代、递归或条件规范的直观构造。这一缺点阻碍了Reo在大规模实际应用中的应用。尽管过去出现了许多受Reo启发的语法替代方案，但它们都没有遵循Reo的主要设计原则：a）声明性规范; b）所有通道类型及其排序都是用户定义的; c）通道通过共享节点组成。在本文中，我们为Reo提供了一个文本语法，它尊重这些原则，并支持灵活的参数传递、迭代、递归和条件规范。在正在进行的工作中，我们使用这种文本语法将Reo编译成目标语言，如Java、Promela和Maude。
A DSL for Mapping Abstract Syntax Models to Concrete Syntax Models in ModelCC
ModelCC是一个基于模型的解析器生成器，它将语言设计与语言处理相结合。ModelCC提供了两种不同的机制来指定从抽象语法模型到具体语法模型的映射：在抽象语法模型规范之上定义的元数据注释和用于定义ASM-CSM映射的域特定语言。使用领域特定语言来指定从抽象语法模型到具体语法模型的映射允许为同一抽象语法模型定义多个具体语法模型。在本文中，我们描述了ModelCC域特定语言的抽象语法模型到具体的语法模型映射，我们展示了它的能力，提供了一个元定义的域特定语言。
Chat2Code: Towards conversational concrete syntax for model specification and code generation, the case of smart contracts
基于模型驱动工程（MDE）框架的自动代码生成工具的革命性潜力尚未实现。除了能够帮助软件专业人员编写更准确、可重用的代码之外，它们还可以使编程对一个全新的非技术用户群体更容易访问。然而，非技术用户接受这些工具的速度很慢。这可能是因为它们的具体语法通常是在文本或图形界面的操作之后模式化的。这些接口是通用的，但用户需要比想象中更广泛、更精确和更详细的知识，才能将其作为具体的语法使用。对话界面（聊天机器人）为非技术用户提供了一种更容易访问的方式来生成代码。在本文中，我们讨论了在模型驱动工程（MDE）框架中集成会话代理的基本挑战，然后转向一个特定的应用：由非技术用户基于会话语法自动生成多种语言的智能合约代码。我们演示了如何做到这一点，并通过进行用户体验调查来评估我们的方法，以评估聊天机器人框架的可用性和功能。
Designing text representations for existing data using the TextFormats Specification Language
TextData是一个用于高效和用户友好地创建文本格式规范的软件系统，可从多种程序设计语言（C/C++，Python，Nim）和Unix命令行访问。要使用格式，必须创建以文本编辑器的规约语言（TFSL）编写的规范。该规范为格式的每个部分定义了数据库。TextData规范中数据类型定义的语法基于文本表示。因此，该系统非常适合于现有格式的描述。然而，当创建一个新的文本格式来表示现有数据时，用户可以根据值的类型和表示选项使用不同的可能定义。本研究探讨了可能的定义语法的文本的规约语言用于创建标量值（例如字符串，数值，布尔）和复合数据结构（例如数组，映射）的文本表示。分析的结果系统地提出，连同每一种类型的不同的值，可以表示的例子，和使用建议。
Functional programming with lambda-tree syntax
我们提出了一个新的功能性程序设计语言，MLTS，使用的数据树语法的方法来编码绑定出现在数据结构的设计。在这种方法中，绑定永远不会成为自由的，也不会脱离它们的范围：相反，数据结构中的绑定被允许移动到程序中的绑定。MLTS的设计在程序中包含了额外的站点，这些站点直接支持绑定的移动。为了正式定义语言的操作语义，我们提出了一个抽象的语法MLTS和一个自然的语义评估。我们将把这样的自然语义看作是一个丰富逻辑中的逻辑理论，这个逻辑包括 * 名义抽象 * 和 *nabla-quantifier*：因此，MLTS的自然语义规范可以给出一个简洁而优雅的表示。我们提出了一个类型化的原则，自然地扩展了核心ML程序的类型化，我们通过几个例子来说明MLTS的功能。本文简要介绍了一个MLTS的联机解释器。
A Denotational Engineering of Programming Languages
这本书致力于两个研究领域：（1）设计程序设计语言以及它们的指称模型。一种语言的指称模型由两个多排序的代数--一个语法代数和一个指称代数--以及一个从语法到指称的（唯一的）同态组成，称为语言的语义。(2)用指称模型为语言设计合理的程序构造器。在我们的方法程序语法包含其完全正确性规范。如果一个程序的说明是正确的，那么它就是正确的。如果给定正确的组件程序产生正确的结果程序，则程序构造器是可靠的。这两种方法都说明了一个例子语言Lingua。
Substitution for Non-Wellfounded Syntax with Binders through Monoidal Categories
本文在范畴论框架下利用幺半范畴和强函子，为非良基绑定语法构造了单子替换操作，并在 Coq 的 UniMath 库中完成形式化验证。
The ModelCC Model-Driven Parser Generator
语法导向的翻译工具需要通过形式语法来规范语言。该语法必须符合要使用的解析器生成器的特定要求。然后，该语法被标注有语义动作，以使结果系统执行其期望的功能。在本文中，我们介绍了ModelCC，基于模型的解析器生成器，从语言处理的语言规范，避免了语法驱动的解析器生成器所造成的一些问题。ModelCC接收一个概念模型作为输入，以及注释它的约束。然后它能够为所需的文本语法创建一个解析器，生成的解析器完全自动化语言概念模型的实例化。ModelCC还包括一个引用解析机制，因此ModelCC能够实例化抽象语法图，而不仅仅是抽象语法树。
The ModelCC Model-Based Parser Generator
形式语言让我们精确地定义数据的文本表示。形式语法，通常以BNF的形式产生，描述语言语法，然后注释语法导向的翻译，并完成语义动作。除了数据的文本表示之外，当需要相应的数据结构的显式表示时，语言设计者必须设计合适的数据模型与其适当的语言规范之间的映射，然后开发从解析树到数据模型实例的转换过程。不幸的是，无论何时必须修改文本表示的格式，更改都必须在整个语言处理器工具链中传播。这些更新非常耗时、乏味且容易出错。此外，如果不同的应用程序使用相同的语言，则必须维护相同语言规范的多个副本。在本文中，我们介绍了ModelCC，基于模型的解析器生成器，从语言处理的语言规范，从而避免了语法驱动的解析器和解析器生成器所造成的许多问题。ModelCC在解析过程中引入了引用解析。因此，ModelCC能够从输入字符串中获取抽象语法图，而不是返回抽象语法树。
Reasoning with Higher-Order Abstract Syntax in a Logical Framework
基于具有更高类型量化的直觉或线性逻辑的逻辑框架已成功地用于对程序设计语言和推理系统领域中的许多重要判断给出高级、模块化和形式化的规范。给定这样的规范，考虑证明框架中指定系统的属性是很自然的：例如，给定函数式程序设计语言的求值规范，证明该语言是确定性的或求值保留类型。开发这种推理框架的一个挑战是高阶抽象语法（HOAS），一种优雅的和声明性的对象级抽象和替换处理，很难在涉及归纳的证明中处理。在本文中，我们提出了一个元逻辑，可用于推理使用HOAS编码的判断，这个元逻辑是一个简单的直觉主义逻辑，承认高阶量化简单类型的非线性项（HOAS的关键成分），以及归纳和定义的概念的扩展。我们通过考虑直觉和线性逻辑的编码，探讨了HOAS编码的形式元理论分析的困难，并正式推导出这些逻辑的重要子集的割的容许性。然后，我们提出了一种方法，以避免高阶抽象语法的好处和分析所产生的编码的能力之间的明显的权衡。我们通过涉及简单函数式和命令式程序设计语言PCF和PCF：=的示例来说明这种方法。我们正式推导出这样的属性，作为唯一性的类型，主题减少，确定性的评价，和等价的过渡语义和自然语义表示的评价。
The SyGuS Language Standard Version 2.1
本文档定义 SyGuS 2.1 标准，规范语法引导综合问题的输入输出格式，并基于 SMT-LIB 2.6 描述其理论、逻辑规约与文法约束。
LambdaDL: Syntax and Semantics (Preliminary Report)
语义数据推动了许多不同的应用程序，但仍然缺乏适当的集成到程序设计语言中。非类型化访问容易出错，而映射方法不能完全捕获语义数据的概念化。在本文中，我们提出了$λ_{DL}$，一个$λ$演算与修改的类型系统，提供类型安全的集成语义数据。这是通过将描述逻辑集成到用于类型化和数据访问的$λ$演算中来实现的。它围绕着几个关键的设计原则。其中包括（1）使用语义概念化作为类型，（2）这些类型的子类型推断，以及（3）通过确保查询的可满足性以及在$λ_{DL}$中精确地键入查询结果来对数据进行类型检查的查询访问。本文激励使用修改的类型系统的语义数据，它提供了理论基础的描述逻辑的集成，以及$λ_{DL}$的核心形式化规范，包括类型安全的证明。
A Structural and Nominal Syntax for Diagrams
monoidal范畴和图形语言之间的对应关系已经被广泛研究，导致在量子计算和通信，系统理论，电路设计等方面的应用。从分类的角度来看，图可以使用（无名称）组合子来指定，这些组合子具有优雅的等式属性。然而，用于图形结构的常规符号，诸如硬件描述语言（VHDL、Verilog）或图形语言（Dot），使用不同的风格，其是平面的、关系的并且依赖于名称（标签）的广泛使用。这样的语言不知道享受好的语法等式属性。然而，由于它们使得指定（和修改）任意图形结构相对容易，因此它们比组合子样式更受欢迎。在本文中，我们将展示如何在不改变语义和现有的等式理论的情况下，两种方法图语法可以调和和统一。此外，我们还对组合句法给出了合理而完整的等式理论。
Aquarium: Cassiopea and Alewife Languages
本技术报告描述了Aquarium内核代码合成项目中使用的两种特定于领域的语言。它以抽象语法的形式呈现了语言的核心。Cassiopea是一种机器描述语言，用于描述处理器指令集的语义。Alewife是一种规约语言，可用于为汇编级指令块编写与机器无关的规约。Alewife规范可用于验证和合成Cassiopea中描述的任何机器的代码，给出规范中使用的抽象的特定于机器的翻译。本文不包括介绍水族馆系统或语言的使用。除了这个版本的文章是一个草案，水族馆项目和语言正在进行中。这一条款目前不能被认为是最后的或完整的。
Industrial Experience Report on the Formal Specification of a Packet Filtering Language Using the K Framework
许多项目专用语言，包括特别是过滤语言，是使用以自然语言编写的非正式规范来定义的。这导致了这些语言规范中的歧义和错误。本文报道了一个工业实验上使用的工具支持的语言规范框架（K）的过滤语言的语法和语义的正式规范具有类似的复杂性，现实生活中的项目。这个实验的目的是估计，在一个特定的工业环境中，正式指定一个包过滤语言使用工具支持的正式方法的困难和好处。
A formal specification of the jq language
本文为 jq 语言的一个大型子集给出了形式化语法和指称语义，并提出了一种新的更新解释方法，以提升执行的可预测性与性能。
Towards Generic Refactoring
我们在研究程序重构时，将语言甚至编程范式作为一个参数。我们使用类型化函数程序，即Haskell程序，作为相应重构框架的规范介质。为了将我们自己从语言语法中分离出来，我们的规范遵循以下风格。(I)至于原始算法的程序分析和转换，我们采用通用功能组合支持通用遍历和多态功能的ad-hoc情况下细化。(II)对于重构所涉及的语言抽象，我们设计了一个专用的多参数类。这个类可以被实例化为各种语言中存在的抽象，例如，Java、Prolog或Haskell。
Effective Sequential Protocol Composition in Maude-NPA
协议不是单独工作，而是一起工作，一个协议依赖于另一个协议来提供所需的服务。密码协议中的许多问题都是在这样的组合不正确或没有很好理解时出现的。在本文中，我们讨论了扩展的Maude-NPA语法及其操作语义，以支持动态顺序组合的协议，使协议可以单独指定和组合时需要的。这允许人们在对规范进行最小更改的情况下推理许多不同的组合，以及在性能和易于规范方面改进我们在[18]中提出的早期组合扩展。我们展示了如何组合可以定义和执行象征性的Maude-NPA使用组合的语法和语义。我们还提供了一个实验分析的性能Maude NPA使用的组合语法和语义，并比较它的性能的语法和语义的组合开发在早期的研究。最后，在结论中，我们给出了一些经验教训的最佳方式扩展基于窄的状态可达性工具，以及与相关的工作和未来的计划进行比较。
Describing the syntax of programming languages using conjunctive and Boolean grammars
Floyd的一个经典结果（“On the non-existence of a phrase structure grammar for ALGOL 60”，1962）指出，任何合理的程序设计语言的完整语法都不能用普通的形式语法（乔姆斯基的"context-free“）来描述。本文使用的语法扩展与合取和否定运算符，被称为合取语法和布尔语法，描述了一个简单的无类型的过程程序设计语言的一组格式良好的程序。一个完整的布尔文法，它定义了这样的概念，作为声明的变量和函数之前，他们的使用，构造和解释。使用用于布尔文法的广义LR解析算法，然后可以在时间上解析程序的长度$O(n^4)$，而另一已知算法允许子时间解析。接下来，它是如何将这种语法转换为一个明确的合取语法，平方时间解析。这显然成为完全由计算上可行的形式文法对程序设计语言的语法的第一个规范。
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方法显着简化了绑定结构的表示，操作，分析和推理。
A Specification's Realm: Characterizing the Knowledge Required for Executing a Given Algorithm Specification
本文提出算法规范的“领域”概念，刻画执行智能体独立执行算法规范所需的前置知识，说明其生成可部分由大语言模型自动化，该刻画可助力算法的多系统实现与形式化验证，并探讨了执行忠实度评估问题。
Syntax and Semantics of Linear Dependent Types
本文提出了一种类型论，它把（直觉）线性类型与类型依赖相结合，从而适当地推广了直觉依赖类型论和完全线性逻辑。语法和完整的范畴语义的发展，后者在（严格）索引对称monoidal范畴的理解。以模块化方式处理各种可选类型的成形器。特别是，我们将看到，历史上备受争议的乘法量词和身份类型自然地产生于范畴考虑。这些新的乘法连接词的进一步特点是由几个身份有关的依赖类型论和线性逻辑通常的连接词。最后，详细研究了一类重要的模型，即由值在某个对称monoidal范畴内的族给出的模型。
Reasoning in Abella about Structural Operational Semantics Specifications
讨论了Abella系统支持的结构化操作语义风格规范的推理方法。该方法使用lambda树语法来处理对象语言绑定，并在泛型判断中编码绑定相关属性。此外，对象语言规范通过递归定义直接嵌入到推理框架中。通过泛型判断来处理绑定隐含地在用于绑定变量的名称中强制执行独特性和原子性。然而，这些属性必须在推理任务中明确。这个目标可以通过允许递归定义也指定原子谓词的通用属性来实现。这些不同的逻辑功能在阿贝拉系统的效用是通过实际的推理任务证明。与其他几个基于逻辑的方法进行了简要的比较。
From Semantics to Syntax: A Type Theory for Comprehension Categories
针对理解范畴中类型间非平凡态射未被标准Martin-Löf类型理论利用的问题，提出内化该态射的类型理论（含Π-、Σ-和恒等类型），可视为带强制子类型的扩展，定义语义结构并证明可靠性，提供大量解释实例。
String Diagrams for $λ$-calculi and Functional Computation
本教程以系统方式介绍高阶计算的字符串图与图语言，从范畴论概念的二维语法逐步深入到笛卡尔闭范畴，通过从范畴模型重构分层超图语法并探讨其在编程语言领域的应用。
Towards the Formal Specification and Verification of Maple Programs
在本文中，我们提出了我们正在进行的工作和初步结果的形式规范和验证的MiniMaple（一个重要的子集Maple轻微扩展）程序。我们工作的主要目标是在这些程序中找到行为错误。通过静态分析确定其规格。这项任务是更复杂的广泛使用的计算机代数语言，如Maple，因为这些是从根本上不同于经典的语言：它们支持非标准类型的对象，如符号，未评估的表达式和多项式，并需要抽象的计算机代数概念和对象，如环和排序等作为一个出发点，我们已经定义和形式化的语法，语义，类型系统和规约语言的MiniMaple。
P4-SpecTec: Integrating a Language Mechanization Framework into the Real-World P4 Specification
该研究提出P4-SpecTec，将语言机械化框架应用于P4，通过算法推理规则实现可执行的P4语义，发现24个错误，其被有条件采用为P4官方规范创作工具链。
Syntax and Semantics of Abstract Binding Trees
本文的贡献是多排序名义抽象绑定树（abts）的语法和语义的发展，二阶泛代数的扩展，以支持符号索引家庭的运营商。名词性abts对于正确处理具有生成现象的语言的句法，包括异常和可变状态是必不可少的。此外，我们已经开发了抽象绑定树的分类语义，正式在建设性类型论使用Agda证明助手。多排序的名词性abt也形成了即将到来的JonPRL证明助手版本的句法基础，JonPRL是Nuprl传统中扩展的构造性类型论的实现。
Categorical Message Passing Language (CaMPL): Syntax and Semantics
本文提出基于线性 actegories 设计的函数式并发语言 CaMPL，赋予程序无死锁及无活锁性质，并通过示例展示其类型系统，编译器已用 Haskell 实现。
Caruca: Effective and Efficient Specification Mining for Opaque Software Components
Caruca利用大型语言模型和系统调用拦截，自动挖掘不透明命令的规格，在60个命令上几乎全部正确，消除了手动工作。
Modules over relative monads for syntax and semantics
我们给出了一类变量绑定语言的语法和语义的代数刻画。我们引入了一个2-签名的概念：这样的签名不仅指定了语言的术语，而且还指定了这些术语的归约规则。对于任何2-签名$S$，我们关联$S$的“模型”类别。这个范畴有一个初始对象，它整合了由$S$自由生成的项，并配备了根据$S$中给出的不等式的约简。我们将这个初始对象称为由$S$生成的语言。2-签名的模型是从相对单子和这些单子上的模块构建的。通过使用单子，模型-特别是初始模型-配备了一个替换操作，该操作在适当的意义上与归约兼容。初始性定理在证明助手Coq中被形式化，产生一种机器，当被馈送2-签名时，该机器为相关的程序设计语言提供约简关系和经认证的替换。
GPU accelerated program synthesis: Enumerate semantics, not syntax!
本文探讨了在GPU上实现基于搜索的程序合成器，通过利用公式语义最小化数据移动和减少依赖数据的分支等GPU友好技术，使合成器能处理更大规模问题且速度远超此前基于CPU的最先进方法。
A Category Theoretic View of Contextual Types: from Simple Types to Dependent Types
本文利用预层模型和余单子 $\ lat$ 刻画 Cocon 的上下文类型语义，并借助带族范畴将其扩展到依赖类型。
Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference
本文引入综合基准 FormalBench 评估 LLM 对程序语义的推理能力，发现其在复杂结构（如循环）和语义保持变换上表现不佳，并设计自修复提示将成功率提升 25%。
2-Functoriality of Initial Semantics, and Applications
本文研究初始语义在不同单调范畴下的2-范畴结构，探讨变量绑定语言模型的比较与关联，提出通用的递归原理。
BODHI: Precise OS Kernel Specification Inference
提出一种领域知识提示方法BODHI，通过结构化C到Python翻译指南增强少样本提示，在OSV-Bench基准上将Pass@1从55.10%提升至96.73%，缩小了通用代码生成与形式规范合成之间的差距。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。