Syntax and Semantics of Cedille
Aaron Stump, Christopher Jenkins
本文介绍了Cedille的语法、分类规则、可实现语义和可靠性定理，Cedille是一个外部的（即，Curry风格）类型论，扩展了构造演算，设计用于推导归纳数据集，并具有归纳原理。
This document presents the syntax, classification rules, realizability semantics, and soundness theorem for Cedille, an extrinsic (i.e., Curry-style) type theory extending the Calculus of Constructions, and designed for deriving of inductive datatypes, with their induction principles.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Syntax and Typing for Cedille Core
本文档指定了Cedille工具中实现的类型论的核心版本。Cedille是一种用于依赖类型编程和计算机检查证明的语言。Cedille可以将源程序细化到Cedille核心，可以通过一个小检查器以简单的方式检查（Cedille包含的参考实现不到1000行Haskell）。其他工具也可以将CedilleCore作为一个富有表现力的后端类型论。该文档描述了Cedille Core的语法和类型规则。
A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille
Cedille是一个相对较新的工具，基于Curry风格的纯类型论，没有原始的数据类型系统。使用新技术的基础上依赖的交叉类型，归纳数据集及其归纳原则。这种方法的一个好处是它允许探索新的或高级形式的归纳数据类型。本文报告的工作进展中的一个这样的形式，即高阶抽象语法（HOAS）。我们在纯类型论的背景下考虑HOAS的性质，与传统的λ演算的环境模型的概念进行比较。我们看到了一种替代方案，基于我们所称的Kripke函数空间，我们可以在Cedille中推导出弱初始代数。使用编码给出了几个例子。
Syntax and analytic semantics of LISA
我们提供了LISA（“石蕊指令集架构”）语言的语法和语义。并行汇编语言LISA在用于模拟弱一致性模型的RISK 7工具（http：//virginia.cs.ucl.ac.uk/RISK/）中实现。
Syntax and semantics of the weak consistency model specification language cat
我们提供的语法和语义的猫语言，一个特定领域的语言来描述并行/分布式程序的一致性属性。该语言也在1997年实现（http：//diy.inria.fr/doc/js.html）。
Syntax and Semantics of Babel-17
我们提出了Babel-17，第一个程序设计语言的纯功能结构化编程（PFSP）。早期的工作说明PFSP的框架中的玩具研究语言。Babel-17通过展示PFSP如何与模式匹配、面向对象编程以及并发、惰性求值、记忆和镜头支持等特性相结合，将这一早期工作提升到了一个新的水平。
Operational Semantics with Hierarchical Abstract Syntax Graphs
这是一个激励教程介绍了语义分析的程序设计语言使用图形语言作为表示的条款，和图形改写作为表示的减少规则。我们展示了如何图形化语言自动结合所需的功能，如阿尔法等价，以及它如何可以描述纯计算，命令式存储，并在一个统一的框架控制功能。图语义结合了结构操作语义和抽象机器的一些最好的特性，同时提供了强大的新方法来推理上下文等价。所有技术细节都可以在Muroya和作者的扩展技术报告以及Muroya的博士论文中找到。
Lolisa: Formal syntax and semantics for a subset of the solidity programming language in Mathematical Tool Coq
本文介绍了为Etheruem区块链平台开发的Solidity程序设计语言的一个大子集的形式语法和语义，基于我们最近开发的一个通用的，可扩展的，可重用的形式内存（GERM）框架和Curry-Howard同构的扩展，表示为执行-验证同构（EVI）。这个子集被表示为Lolisa，据我们所知，它是为Solidity开发的第一个机械化和验证的正式语法和语义。Lolisa的形式语法采用了比Solidity更强大的静态类型系统，以增强类型安全性。此外，Lolisa不仅包含Solidity的几乎所有语法组件，如映射、修饰符、合约和地址类型，而且还包含通用程序设计语言功能，如多个返回值、指针算术、结构和字段访问。因此，Lolisa固有的兼容性允许Solidity程序直接翻译成Lolisa，而无需重建或抽象，并且Lolisa固有的通用性允许它扩展到表达其他程序设计语言。为此，我们还提出了一个初步的计划，系统地扩展到其他语言。
SimP: Unifying Syntax- and Semantic-Guided Techniques for Efficient Program Reduction
SimP框架结合传统与LLM式缩减技术，兼顾缩减效率与质量，且LLM成本可忽略，解决编译器漏洞调试中测试程序过大的问题。
Functional programming with lambda-tree syntax
我们提出了一个新的功能性程序设计语言，MLTS，使用的数据树语法的方法来编码绑定出现在数据结构的设计。在这种方法中，绑定永远不会成为自由的，也不会脱离它们的范围：相反，数据结构中的绑定被允许移动到程序中的绑定。MLTS的设计在程序中包含了额外的站点，这些站点直接支持绑定的移动。为了正式定义语言的操作语义，我们提出了一个抽象的语法MLTS和一个自然的语义评估。我们将把这样的自然语义看作是一个丰富逻辑中的逻辑理论，这个逻辑包括 * 名义抽象 * 和 *nabla-quantifier*：因此，MLTS的自然语义规范可以给出一个简洁而优雅的表示。我们提出了一个类型化的原则，自然地扩展了核心ML程序的类型化，我们通过几个例子来说明MLTS的功能。本文简要介绍了一个MLTS的联机解释器。
LambdaDL: Syntax and Semantics (Preliminary Report)
语义数据推动了许多不同的应用程序，但仍然缺乏适当的集成到程序设计语言中。非类型化访问容易出错，而映射方法不能完全捕获语义数据的概念化。在本文中，我们提出了$λ_{DL}$，一个$λ$演算与修改的类型系统，提供类型安全的集成语义数据。这是通过将描述逻辑集成到用于类型化和数据访问的$λ$演算中来实现的。它围绕着几个关键的设计原则。其中包括（1）使用语义概念化作为类型，（2）这些类型的子类型推断，以及（3）通过确保查询的可满足性以及在$λ_{DL}$中精确地键入查询结果来对数据进行类型检查的查询访问。本文激励使用修改的类型系统的语义数据，它提供了理论基础的描述逻辑的集成，以及$λ_{DL}$的核心形式化规范，包括类型安全的证明。
A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs
几乎每一种编程语言的语法都包含绑定器和相应的绑定事件的概念，以及伴随的$α$等价、避免捕获的替换、类型上下文、运行时环境等概念。在过去，实现和推理程序设计语言需要仔细处理以维护绑定变量的正确行为。现代程序设计语言包含了一些特性，这些特性使得像范围安全这样的约束可以用类型来表达。尽管如此，程序员仍然被迫为范围安全操作的每个新实现重新编写相同的样板（例如，重命名、取代、脱糖、印刷等），然后再进行正确性证明。我们提出了一个具有约束力的语法表达宇宙，并演示了如何（1）实现范围安全遍历一劳永逸的泛型编程;（2）如何派生这些遍历的属性泛型证明。我们的宇宙描述，一般的遍历和证明，以及我们的例子都已经在Agda中正式化，并且可以在https://github.com/gallais/generic-syntax在线获得的附带材料中获得。
Compositional Semantics for the Procedural Interpretation of Logic
逻辑程序的语义由证明论、模型论和直接后果算子的不动点给出。如果子句逻辑是一种程序设计语言，那么它也应该具有组合语义。程序设计语言的组合语义遵循程序的抽象语法，通过对其组成单元的含义进行数学运算来组成单元的含义。逻辑的过程解释只产生了逻辑程序的不完整的抽象语法。我们完成它，并使用的结果作为基础的组合语义。我们提出比较塔斯基的代数化的一阶谓词逻辑，这是在实质上的组合语义为他选择的语法。我们的特点是我们的语义等价的直接后果运营商。
DSL development based on target meta-models. Using AST transformations for automating semantic analysis in a textual DSL framework
本文描述了一种为领域特定语言（DSL）创建文本语法的方法。我们认为目标元模型是主要的工件，因此要首先开发。其核心思想是将文本语法分析表示为一系列转换。这是由显式操作抽象语法树（ATS），提出了一种简单的语言。文本到模型的转换分为两个部分：文本到AST（由openArchitectureWare [1]开发）和AST到模型（本文提出）。我们的方法简化了语义分析，并有助于生成尽可能多的。
An experiment with denotational semantics
本文介绍了如何按“逆序”，即从表示到语法，系统地设计一门程序设计语言。这种结构是在一个代数框架中开发的，该框架由三个多排序代数组成：表示法，抽象语法和具体语法。这些代数是以这样一种方式构造的，即从具体语法到指称存在唯一的同态，这构成了语言的指称语义。除了它的代数框架，该模型是集合论的，即指称域只是集合，而不是斯科特的自反域。该方法说明了一个虚拟语言Lingua的逐层开发：一个应用层，一个命令层（递归过程）和一个SQL层，其中Lingua被视为一个API（应用程序编程接口）的SQL引擎。后者也被赋予了指称语义。该语言配备了强大的打字机制，涵盖了基本类型（数字，布尔等），列表、数组、记录及其任意组合，以及类似SQL的类型：行、表和数据库。类型模型包括SQL完整性约束。
Yaps: Python Frontend to Stan
Stan是一种流行的概率性程序设计语言，具有接近图形模型的自包含语法和语义。不幸的是，Python中现有的Stan嵌入使用多行字符串。这种方法迫使用户在两种不同的语言风格之间切换，不支持Stan代码中的语法突出显示或简单的错误报告。这篇文章解决了Stan是否可以在使用Python语法的同时保留其自包含的语义的问题。答案是肯定的，这可以通过重新解释Python语法来实现。本文介绍了Yaps，一个基于重新解释的Python的Stan的新前端。我们在超过1000个Stan模型上测试了Yaps，并将其开源。
Towards Cumulative Abstract Semantics via Handlers
本文提出通过作用域效应实现累积抽象语义，以构建模块化且优雅的抽象解释框架。
Syntax and Semantics of Abstract Binding Trees
本文的贡献是多排序名义抽象绑定树（abts）的语法和语义的发展，二阶泛代数的扩展，以支持符号索引家庭的运营商。名词性abts对于正确处理具有生成现象的语言的句法，包括异常和可变状态是必不可少的。此外，我们已经开发了抽象绑定树的分类语义，正式在建设性类型论使用Agda证明助手。多排序的名词性abt也形成了即将到来的JonPRL证明助手版本的句法基础，JonPRL是Nuprl传统中扩展的构造性类型论的实现。
TRANX: A Transition-based Neural Abstract Syntax Parser for Semantic Parsing and Code Generation
我们提出TRANX，一个基于转换的神经语义解析器，映射到正式的意义表示（MR）的自然语言（NL）的话语。TRANX使用基于目标MR的抽象语法描述语言的转换系统，这给它带来了两个主要优点：（1）它是高度精确的，使用来自目标MR的语法的信息来约束输出空间并对信息流建模，以及（2）它是高度可概括的，并且可以很容易地应用于新类型的MR，只需编写与MR中允许的结构相对应的新的抽象语法描述。在四个不同的语义解析和代码生成任务上的实验表明，我们的系统是可推广的，可扩展的，有效的，与现有的神经语义解析器相比，注册强大的结果。
Kayak: Safe Semantic Refactoring to Java Streams
重构是对现有软件的结构化更改，使其外部可观察的行为保持不变。其目的是提高可读性、性能或其他非行为属性。最先进的自动重构工具是语法驱动的，因此过于保守。在本文中，我们将探讨语义驱动的重构，这使得更复杂的重构模式。作为这个更广泛的想法的一个例子，我们提出了Kayak，一个自动重构工具，它将Java与外部迭代集合转换为使用Streams的代码，Streams是Java 8引入的一个新抽象。我们的重构过程执行语义推理和搜索的空间中可能的重构使用自动程序合成。我们的实验结果支持的猜想，语义驱动的重构更精确，能够重写更复杂的代码场景相比，语法驱动的重构。
Case Studies in Formal Reasoning About Lambda-Calculus: Semantics, Church-Rosser, Standardization and HOAS
我们以前已经出版了Isabelle/HOL形式化的一般理论的语法绑定。在这篇配套文件中，我们实例化的一般理论，以语法的λ演算和形式化的发展，导致几个基本的结构和结果：健全的语义解释，教会罗瑟和标准化定理，高阶抽象语法（HOAS）编码。对于Church-Rosser和标准化，我们的工作涵盖了微积分的按名称调用和按值调用版本，遵循Takahashi和Plotkin的经典论文。在形式化过程中，我们能够专注于开发的高级思想-感谢我们的一般理论提供的武器库：关于替换，交换和新鲜度操作符的丰富基本事实，以及递归定义和推理原则，包括语法语义解释的专业化。
Initial Semantics for Strengthened Signatures
我们给出了一个新的arity的一般定义，产生的同伴签名和相关的语法的概念。这种设置在Ghani和Uustalu所要求的意义上是模块化的：合并两个语法扩展对应于构建一个合并的总和。这些签名太笼统了，因为我们无法证明在这个一般上下文中存在相关语法。所以我们必须选择存在所需初始单子的节点和签名。为此，我们遵循Matthes和Uustalu开辟的轨道：我们引入了加强arity的概念，并证明了相应的签名具有初始语义（即关联语法）。我们的加强型定理允许上极限，它允许用显式替换来处理λ-演算。
Syntax and Semantics of Linear Dependent Types
本文提出了一种类型论，它把（直觉）线性类型与类型依赖相结合，从而适当地推广了直觉依赖类型论和完全线性逻辑。语法和完整的范畴语义的发展，后者在（严格）索引对称monoidal范畴的理解。以模块化方式处理各种可选类型的成形器。特别是，我们将看到，历史上备受争议的乘法量词和身份类型自然地产生于范畴考虑。这些新的乘法连接词的进一步特点是由几个身份有关的依赖类型论和线性逻辑通常的连接词。最后，详细研究了一类重要的模型，即由值在某个对称monoidal范畴内的族给出的模型。
From Semantics to Syntax: A Type Theory for Comprehension Categories
针对理解范畴中类型间非平凡态射未被标准Martin-Löf类型理论利用的问题，提出内化该态射的类型理论（含Π-、Σ-和恒等类型），可视为带强制子类型的扩展，定义语义结构并证明可靠性，提供大量解释实例。
Modules over relative monads for syntax and semantics
我们给出了一类变量绑定语言的语法和语义的代数刻画。我们引入了一个2-签名的概念：这样的签名不仅指定了语言的术语，而且还指定了这些术语的归约规则。对于任何2-签名$S$，我们关联$S$的“模型”类别。这个范畴有一个初始对象，它整合了由$S$自由生成的项，并配备了根据$S$中给出的不等式的约简。我们将这个初始对象称为由$S$生成的语言。2-签名的模型是从相对单子和这些单子上的模块构建的。通过使用单子，模型-特别是初始模型-配备了一个替换操作，该操作在适当的意义上与归约兼容。初始性定理在证明助手Coq中被形式化，产生一种机器，当被馈送2-签名时，该机器为相关的程序设计语言提供约简关系和经认证的替换。
Presentable signatures and initial semantics
本文提出可呈现签名框架，用于指定数据类型和编程语言语法，通过初始语义生成语法，涵盖变量绑定并支持组合构造，且经计算机验证。
DRReduce: Enhancing Syntax-Guided Program Reduction with Dependency Reconstruction
本文提出DRReduce框架，通过在语法引导缩减中加入轻量级的语义层依赖重建，修复因删除而断裂的程序依赖，从而保持中间程序的语义有效性并提高属性检查器的接受率。
Searching for Programmatic Policies in Semantic Spaces
本文提出在程序语义空间而非语法空间中进行策略合成搜索，通过学习行为多样的程序库并定义邻域函数实现，在MicroRTS中验证了该方法具有更高的样本效率。
Dynamic Neural Program Embedding for Program Repair
神经程序嵌入已经显示出了很大的希望，最近的各种程序分析任务，包括程序合成，程序修复，故障定位等，然而，大多数现有的程序嵌入是基于程序的语法特征，如原始令牌序列或抽象语法树。与图像和文本不同，程序具有明确的语义含义，仅考虑其语法可能难以捕获（即，语法相似的程序可能表现出截然不同的运行时行为），这使得基于语法的程序嵌入从根本上受到限制。本文提出了一种新颖的语义程序嵌入，它是从程序执行轨迹中学习的。我们的关键见解是，表示为实时变量值的顺序元组的程序状态不仅更精确地捕获程序语义，而且还为递归神经网络建模提供了更自然的拟合。我们评估不同的语法和语义程序嵌入预测的错误类型，学生在提交给一个入门编程类和两个练习CodeHunt教育平台。评估结果表明，我们的新的语义程序嵌入显着优于基于令牌序列和抽象语法树的语法程序嵌入。此外，我们增加了基于搜索的程序修复系统，从我们的se-mantic嵌入获得的预测，并显示搜索效率也显着提高。
Context-Aware Parse Trees
Aroma是一种最先进的代码推荐系统，它提出的简化解析树（SPT）是一种树结构表示，用于通过捕获程序\emph{structure}而不是程序\emph{syntax}来推断代码语义。这与主要由程序设计语言语法驱动的经典抽象语法树不同。虽然我们相信语义驱动的表示是可取的，一个SPT的建设的细节可以影响其性能。我们分析了这些细微差别，并提出了一个新的树结构，严重影响芳香的SPT，称为\emph{context-aware parse tree}（CAPT）。CAPT通过提供更丰富层次的语义表示来增强SPT。具体地说，CAPT为特定于语言的技术提供了额外的绑定支持，用于添加语义突出的功能，并为语言无关的技术提供了额外的绑定支持，用于删除语法上存在但语义上不相关的功能。我们的研究定量地证明了我们提出的语义显著特征的价值，使特定的CAPT配置在我们分析的48，610个程序中比SPT准确39%。
Syntax and semantics of focalisation with relative monads and comonads
本文研究直觉主义与线性设置中资源与效应模态的焦点化语法，通过相对（余）单子实现线性call-by-push-value模型中模态的完备性，并从非结合范畴的伴随角度建立对应关系。
GPU accelerated program synthesis: Enumerate semantics, not syntax!
本文探讨了在GPU上实现基于搜索的程序合成器，通过利用公式语义最小化数据移动和减少依赖数据的分支等GPU友好技术，使合成器能处理更大规模问题且速度远超此前基于CPU的最先进方法。
Useful Evaluation: Syntax and Semantics (Technical Report)
本工作首次归纳定义有用CBV求值的UCBV策略，证明其为LCBV的可靠完备优化实现，通过系统U提供首个语义模型并刻画终止性，还关联GLAMoUr抽象机确立时间不变性。
Effective Sequential Protocol Composition in Maude-NPA
协议不是单独工作，而是一起工作，一个协议依赖于另一个协议来提供所需的服务。密码协议中的许多问题都是在这样的组合不正确或没有很好理解时出现的。在本文中，我们讨论了扩展的Maude-NPA语法及其操作语义，以支持动态顺序组合的协议，使协议可以单独指定和组合时需要的。这允许人们在对规范进行最小更改的情况下推理许多不同的组合，以及在性能和易于规范方面改进我们在[18]中提出的早期组合扩展。我们展示了如何组合可以定义和执行象征性的Maude-NPA使用组合的语法和语义。我们还提供了一个实验分析的性能Maude NPA使用的组合语法和语义，并比较它的性能的语法和语义的组合开发在早期的研究。最后，在结论中，我们给出了一些经验教训的最佳方式扩展基于窄的状态可达性工具，以及与相关的工作和未来的计划进行比较。
Categorical Message Passing Language (CaMPL): Syntax and Semantics
本文提出基于线性 actegories 设计的函数式并发语言 CaMPL，赋予程序无死锁及无活锁性质，并通过示例展示其类型系统，编译器已用 Haskell 实现。
The Syntax and Semantics of einsum
本文针对 einsum 缺乏统一理论基础的问题，形式化定义其语言，并证明张量表达式的关键等价规则，为推理与优化提供依据。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。