Deriving Law-Abiding Instances
Liquid Haskell的精化-反射特性增强了Haskell语言的定理证明功能，允许程序员使用证明来改进现有代码。但是，这些证明中的许多都需要编写繁琐的常规样板代码。此外，许多这样的证明不能很好地扩展，因为证明项的大小可以随着证明中涉及的数据集的大小而超线性地增长。我们提出了一种技术，利用数据类型通用编程，解决了这个问题，细化反射编程。我们的观察是，我们可以采用任何代数数据类型，生成等价的表示类型，并让Liquid Haskell自动构造（并证明）原始类型和表示类型之间的同构。这减少了许多证明到简单的代数“积木”类型上的简单定理，允许程序员便宜而愉快地编写通用证明。
2017-08-07 cs.LO cs.PL
LibNDT: Towards a Formal Library on Spreadable Properties over Linked Nested Datatypes
在过去的25年里，嵌套数据库得到了广泛的研究，无论是在理论上使用范畴理论，还是在程序设计语言（如Haskell）中的实践。它们存在于递归多态数据库中，其中类型参数在整个递归过程中都在变化。它们有多种应用，例如对常规数据类型进行内存建模或约束建模，而不依赖于依赖类型。在这项工作中，我们专注于一个特定的子集，我们称之为链接嵌套数据类型（LNDT）的嵌套数据库。我们表明，一些常见的datashees，如列表和也许，以及一些著名的嵌套datashees，如巢，甚至布什可以建立各种实例的LNDT。我们继续介绍LibNDT，一个库，在Agda和Coq开发，它侧重于一组结构，可以直接从LNDT建立的参数传播到LNDT本身。这些可展开的元素有两种，一种是功能，如折叠和映射，另一种是属性，如映射的全等性或对结构中至少一个或全部元素的给定谓词的满足。我们利用Coq和Agda的依赖类型系统来建模后者。本文最后讨论了在我们的开发过程中提出的各种有趣的话题，例如终止问题，我们的工具的比较以及使用其他元素扩展LibNDT所需的证明工作。
2022-07-02 cs.LO cs.PL
Generic Zero-Cost Reuse for Dependent Types
众所周知，依赖类型语言在代码重用方面存在问题。传统的非索引代数数据库（例如列表）与大量的索引变量（例如向量）一起出现。函数经常被重写为基本相同数据类型的非索引和索引版本，这是代码重复的来源。我们在Curry风格的依赖类型论中工作，其中相同的未类型化术语可以被分类为数据类型的非索引版本和索引版本。对于依赖类型的重用问题，已经提出了许多解决方案，但是我们在解决方案中利用Curry风格的类型论，不仅重用数据和程序，而且以零成本（没有运行时损失）这样做。我们的工作是一个练习依赖类型的泛型编程，并内化的过程中的零成本重用的身份功能的咖喱风格的理论。
2018-07-09 cs.PL
Seamless, Correct, and Generic Programming over Serialised Data
本文提出利用Idris中的QTT定义序列化数据类型宇宙，提供处理缓冲区数据的通用程序，并通过构造IO函数证明其完全功能正确性。
2024-04-26 cs.PL
Gemini: A Functional Programming Language for Hardware Description
本文介绍了双子座，功能程序设计语言的硬件描述，提供的功能，如参数多态性，递归数据库，高阶函数，和类型推断更高的表达能力相比，现代硬件描述语言。Gemini通过其独特的类型系统（由多个原子类型和依赖类型组成）演示了新颖的类型理论概念的理论和实现，该类型系统允许该语言安全地对软件和硬件构造进行建模，并通过多阶段编译执行类型推断。本文的主要技术成果包括形式化的双子座语法，类型规则，和评估规则，双子座的类型系统的安全性证明，和编译器的语义分析阶段的原型实现。
2019-11-10 cs.PL
Generic Programming in OCaml
我们提出了一个通用编程在OCaml库，适应一些技术借鉴其他函数式语言。该库利用了OCaml最近增加的三个功能：通用抽象数据库对于反映类型是必不可少的，可扩展的变体允许这种反映对新的添加开放，扩展点提供语法糖并生成简化库使用的样板代码。该库的构建块可用于通过视图的概念支持许多泛型编程方法。泛型遍历是在库的顶部实现的，并提供强大的组合子来编写复杂树类型上递归函数的简洁定义。我们的案例研究是一个尊重类型抽象的类型安全函数。
2018-12-31 cs.PL
An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes
University of California, Berkeley（加利福尼亚大学伯克利分校）
针对现有SMT求解器处理代数数据类型（ADTs）时因惰性方法导致扩展性差的问题，提出一种急切方法，将ADT查询归约为未解释函数（UF）理论，并证明了该方法的可靠性、完备性及优于现有方法的性能。
2023-10-18 cs.AI cs.LO cs.PL
Unboxing Mutually Recursive Type Definitions in OCaml
在现代OCaml中，单参数数据类型声明（具有单个构造函数的变量，具有单个字段的记录）有时可以“取消装箱”。这意味着它们的内存表示与它们的单个参数相同（省略了变量或记录构造函数和间接），从而实现了更好的时间和内存效率。然而，在广义/保护代数数据库（GADT）的情况下，由于对OCaml值的运行时表示的微妙假设，拆箱并不总是可能的。目前的正确性检查是不完整的，拒绝了许多有效的定义，特别是那些涉及相互递归的数据类型声明。在本文中，我们解释了分离性的概念作为一个语义的拆箱标准，并提出了一套推理规则来检查分离性。从这些推理规则中，我们得到了一个新的实现的拆箱检查，正确地支持相互递归的定义。
2018-12-12 cs.PL
Elaborating Inductive Definitions
我们提出了一个归纳定义的阐述下到一个宇宙的数据。数据域是类型论中严格正族的内部表示。通过将一个归纳定义--一个句法人工产物--细化到它的代码--它的语义--我们得到了一个在类型论本身内部的归纳解释：我们声称关于归纳定义的推理可以在类型论中进行，而不是像通常那样在元理论中进行。此外，我们给出了一个形式化的详细说明过程。因此，它也服从形式推理。我们证明了我们的翻译的合理性，并暗示其正确性与科克的归纳定义。这种方法的实际好处是多方面的。对于类型理论家来说，这是迈向自举的一小步。在类型论本身中实现归纳片段。对于程序员来说，这意味着更好地支持泛型编程：我们将提出一个轻量级的派生机制，完全由程序员定义，因此不需要对类型论进行任何扩展。
2012-10-30 cs.PL
Dependent Types in Haskell: Theory and Practice
在Glasgow Haskell编译器（GHC）中实现的Haskell已经添加了新的类型级编程特性一段时间了。这些特性中的许多--主要是：广义代数数据库（GADT）、类型族、种类多态性和提升数据库--已经将Haskell带到了依赖类型的门槛。许多依赖类型的程序现在甚至可以被编码，但是构造过程通常是痛苦的。在这篇论文中，我描述了依赖Haskell，它通过对今天的Haskell的向后兼容扩展来支持完全依赖类型。这项工作的一个重要贡献是在GHC中实现了Dependent Haskell的一部分，其余部分将遵循。我实现的特性已经在GHC 8.0中发布了。本论文包含了依赖Haskell代码的几个实际例子，依赖Haskell和今天的Haskell之间的差异，一个新的类型安全的依赖类型的类演算（称为Pico）适合用作编译依赖Haskell的中间语言，和一个类型推断和细化算法，烘烤，翻译依赖Haskell类型正确的Pico之间的完整描述。
2017-08-12 cs.PL
A General Framework For Lazy Functional Logic Programming With Algebraic Polymorphic Types
我们提出了一个一阶函数逻辑编程的一般框架，支持懒惰的功能，非确定性和多态数据库，其数据构造器服从一组C的方程公理。在给定的C之上，我们指定一个程序作为定义函数的基于C的条件重写规则的集合R。我们认为，等式逻辑不提供适当的语义，这样的程序。因此，我们提出了一个替代逻辑，其中包括基于C的重写演算和模型的概念。我们得到了基于C的重写w.r.t.的可靠性和完整性。模型，所有程序的自由模型的存在，以及类型保留结果。作为操作语义，我们开发了一个完善的目标求解过程，该过程基于懒惰收缩与模C统一的结合。我们的框架是相当有表现力的许多目的，如解决行动和变化的问题，或实现的伽马计算模型。
2004-04-24 cs.PL
Code Reuse With Transformation Objects
我们提出了一个轻量级的数据类型泛型编程的ObjectiveCaml程序设计语言，旨在更好的代码重用的方法。我们表明，通常通过递归函数与模式匹配表示的一大类变换可以使用单个每类型遍历函数和一组对象编码的变换来实现，我们称之为变换对象。对象编码允许以传统的面向对象方式修改、继承和扩展转换。然而，数据表示保持不变，这保留了以通常方式构造和模式匹配它的能力。我们的方法同样适用于常规和多态变体类型，这使得它可以结合数据类型和它们的转换从静态类型和单独编译的组件。我们还提出了一个实现，它允许我们自动派生的大部分功能，从一个稍微增强的类型描述。
2018-02-06 cs.PL
Denotational cost semantics for functional languages with inductive types
分析函数程序的渐近复杂性的一个主要方法是提取并求解一个以输入大小表示评估成本的递推公式。输入大小的相关概念通常特定于数据类型，其度量包括列表的长度，列表中的最大元素和树的高度。在这项工作中，我们给出了一个正式的帐户提取成本和大小递归高阶函数程序归纳datastries。我们的方法允许广泛的程序员指定的大小的概念，并确保提取的递归正确预测评估成本。为了从程序中提取递归，我们首先通过应用从源语言到复杂性语言的一元转换来明确成本，然后将数据类型值抽象为大小。大小抽象可以在语义上完成，在复杂性语言的模型中工作，或者在语法上通过向前序判断添加规则来完成。我们给出了几种不同的模型的复杂性语言，支持不同的概念的大小。此外，我们证明了一个逻辑关系的参数，递归提取的这个过程是评估成本的上限，证明是完全语法，因此适用于我们考虑的所有模型。
2015-06-05 cs.PL
Optimizing Layout of Recursive Datatypes with Marmoset
Marmoset是一个编译器，通过分析递归代数数据类型的使用并求解约束系统来优化其内存布局，生成紧凑、指针追逐少的表示，实验证明其优于Gibbon和MLton。
2024-11-06 cs.PF cs.PL
Designing text representations for existing data using the TextFormats Specification Language
TextData是一个用于高效和用户友好地创建文本格式规范的软件系统，可从多种程序设计语言（C/C++，Python，Nim）和Unix命令行访问。要使用格式，必须创建以文本编辑器的规约语言（TFSL）编写的规范。该规范为格式的每个部分定义了数据库。TextData规范中数据类型定义的语法基于文本表示。因此，该系统非常适合于现有格式的描述。然而，当创建一个新的文本格式来表示现有数据时，用户可以根据值的类型和表示选项使用不同的可能定义。本研究探讨了可能的定义语法的文本的规约语言用于创建标量值（例如字符串，数值，布尔）和复合数据结构（例如数组，映射）的文本表示。分析的结果系统地提出，连同每一种类型的不同的值，可以表示的例子，和使用建议。
2023-01-31 cs.PL cs.SE
Fix Your Types
当使用现有的ACL2数据类型框架时，许多定理需要类型假设。这些假设减慢了定理证明器的速度，写起来很乏味，而且很容易忘记。我们描述了一个原则性的方法，提供强大的类型安全性和执行效率，同时避免类型假设，我们提出了一个库，自动化这种方法。使用这种方法，类型可以帮助您捕获编程错误，然后避开定理证明。
2015-09-21 cs.LO cs.PL
Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages
布尔电路可逆程序设计语言的$\mathitΠ$族被提出作为见证代数数据集类型同构的组合子的语法。在本文中，我们给出了这种语言的指称语义，使用同伦类型论的弱群胚的语言，并展示了如何推导出它的方程理论，由2-组合子证明可逆电路的等价性。我们建立一个对应的语法广群的语言和一个正式提出的有限类型的单叶子宇宙。对应关系1-combinators的1-路径，2-combinators的2-路径在宇宙中，这被证明是健全的和完整的两个层次，建立充分的抽象和充分性。我们已经建立的Curry-Howard对应$\mathitΠ$的可逆逻辑，可逆程序设计语言和对称钻机广群之间的Curry-Howard-Lambek对应，表明语法的$\mathitΠ$是由自由对称钻机广群，有限集和排列。我们的证明使用的技术，从理论的组介绍和重写系统来解决对称群的字的问题。利用我们结果的形式化，我们展示了如何通过评估、验证和合成可逆逻辑门来进行规范化，并以量子计算的示例为动力。
2021-10-11 cs.LO cs.PL
A Domain Theory for Statistical Probabilistic Programming
我们给出了一个足够的指称语义的语言递归高阶类型，连续概率分布，和软约束。这些是用于构建计算统计和机器学习中使用的贝叶斯模型的表达语言。其中包括无类型语言，类似于Church和WebPPL，因为我们的语义允许递归混合方差数据库。我们的语义证明了重要的程序等价性，包括交换性。我们的新语义模型是基于“准Borel predomains”。它们是链完全偏序（cpos）和拟波莱尔空间的混合。拟波莱尔空间是概率论的一个新模型，它主要研究可容许随机元的集合。在cpo模型中，传统上使用概率幂域来处理概率，但不知道这些幂域在任何具有高阶函数的cpo上都是可交换的。相比之下，拟Borel前域支持交换概率幂域和高阶函数。正如我们所示，准Borel predomains形式的菲奥雷的公理域理论和模型的科克的综合措施理论。
2021-07-29 cs.LO cs.PL
A general formal memory framework in Coq for verifying the properties of programs based on higher-order logic theorem proving with increased automation, consistency, and reusability
近年来，许多轻量级程序已被部署在关键领域，例如基于区块链技术的智能合约。因此，这类程序的安全性和可靠性应该由最可信的技术来保证。高阶逻辑定理证明是验证程序性质的最可靠的技术之一。然而，程序可以由不同的高级程序设计语言开发，并且可以同时支持不同的形式化验证规范（特别是在代码级）的通用的、可扩展的和可重用的形式存储器（GERM）框架目前不可用于验证程序的属性。因此，目前的工作提出了一个GERM框架，以填补这一空白。该框架模拟物理内存硬件结构，包括一个低层形式化内存空间，并提供一套简单、非侵入的应用程序编程接口和辅助工具，使用Coq同时支持不同的形式化验证规范。建议的GERM框架是独立的和可定制的，并完全在Coq中验证。我们还提出了一个扩展的Curry-Howard同构，表示为执行-验证同构（EVI），它结合了符号执行和定理证明，以提高自动化程度的高阶逻辑定理证明辅助工具。我们还实现了一个玩具功能的程序设计语言在一个广义代数数据库风格和形式解释器在Coq的基础上GERM框架。这些实现，然后演示了EVI的应用程序到一个简单的代码段。
2018-03-27 cs.PL
Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice
类型论、逻辑框架和元语言构成了设计、实现和推理形式语言及其语义的共同基础。它们是现代程序设计语言、认证软件和特定领域逻辑设计的核心。更广泛地说，它们继续影响着数学、逻辑和计算机科学许多领域的应用。逻辑框架和元语言：理论与实践研讨会旨在汇集设计师，实施者和从业者在这些领域的工作，特别是关于：自动化和实施的元理论的程序设计语言和相关演算;设计证明助手，自动定理证明器，和正式的数字图书馆建立在逻辑框架技术;关于变量绑定和新名称生成的编码的理论和实践问题，特别是从绑定签名定义的数据集的表示和推理;元编程的案例研究，以及程序设计语言和其他演算的描述的（Meta）理论的机械化。本卷包含2010年7月14日在爱丁堡（英国）举行的LFMTP 2010上提交的论文的最终版本和修订版本。LFMTP 2010是联邦逻辑会议（FLoC 2010）的一部分，并与LICS 2010相关联。
2010-09-11 cs.LO cs.PL
Analysis of MiniJava Programs via Translation to ML
MiniJava是面向对象的程序设计语言Java的一个子集。标准ML是函数式程序设计语言ML家族的规范代表，包括F#和OCaml。已经为类Java和类ML语言开发了不同的程序分析和验证工具和技术。当然，为特定语言开发的工具强调准确处理该语言中常用的语言特征。在Java中，这意味着对象具有可变属性和动态方法分派。在ML中，这意味着具有模式匹配的高阶函数和代数数据集。我们建议将程序从一种语言翻译成另一种语言，并使用目标语言的工具进行分析和验证。通过这样做，我们希望确定目标语言的工具中需要改进的地方，并提出可能指导其改进的技术，这些技术可能与源语言的工具中使用的技术一样。更一般地说，我们希望开发用于推理程序的工具，这些工具对代码风格和数据表示的变化更具弹性。我们首先概述了从MiniJava到ML的转换，该转换仅使用ML的核心功能;特别是，它避免了使用ML的可变引用。
2020-12-30 cs.PL
Revisiting Language Support for Generic Programming: When Genericity Is a Core Design Goal
内容：Stepanov定义的泛型编程是一种通过只考虑底层数据类型和操作的必要属性来编写高效和可重用算法的方法。泛型编程已被证明是一种有效的手段，构建可重用的软件组件库的语言，支持它。泛型相关的语言设计的选择发挥了重要作用，如何有利于泛型编程在实践中。询价：几种主流的程序设计语言（如Java和C++）最初都是在没有泛型的情况下创建的;后来逐渐添加了支持泛型编程的特性。因此，关于支持泛型编程的现有文献大多侧重于将泛型编程改造为现有语言，并确定相关的实施挑战。当使用为泛型编程而设计的语言进行编程时，编程体验是否明显更好，或者是否与以前的语言设计选择不同？方法：我们研究Magnolia，一种旨在体现泛型编程的语言。Magnolia是一种基于代数规范的语言设计方法的代表。我们重复了一个著名的实验，通过实现Boost Graph Library的一个子集来仔细检查Magnolia的泛型编程工具，并反思我们的开发经验。知识：我们发现，在以前的研究和工作的主题确定为支持Stepanov风格的泛型编程的关键功能的习惯用法没有告诉一个完整的故事。我们澄清了它们中的哪一个更像是达到目的的手段，而不是支持泛型编程的基本功能。基于Magnolia的开发经验，我们将变元确定为泛型编程的一个附加关键特性，并指出属性泛型的局限性和挑战。接地：我们的工作使用文献中用于评估语言通用编程功能的众所周知的框架来评估Mag…
2022-11-03 cs.PL
Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types
Purdue University（普渡大学）；Tufts University（塔夫茨大学）；Augusta University（奥古斯塔大学）
本文提出了一种算法可达性类型，通过灵活的自我引用和双向类型算法，实现了在复杂对象图中安全跟踪可达性，避免了类型中的非法作用域名称。
2026-06-10 cs.PL
Latent Effects for Reusable Language Components: Extended Version
程序设计语言的开发可能相当复杂和昂贵。因此，许多努力都致力于语言功能的模块化定义，可以在各种组合中重用，以定义新的语言并对其语义进行实验。这些努力的一个显著成果是基于代数的“点菜数据库”方法。当与代数效应相结合时，DTC可以对广泛的公共语言特征进行建模。不幸的是，目前的技术水平不包括高级控制流机制的模块化定义，这些机制将执行推迟到适当的点，例如按名称调用和按需要调用评估以及（多）分段。本文定义了潜在的影响，一类通用的控制流机制。我们演示了函数抽象，懒惰计算和MetaML的分期都可以表示在一个模块化的方式使用潜在的影响，以及如何将它们以各种方式组合起来，以获得复杂的语义。我们提供了我们的效果和处理程序的完整Haskell实现，并提供了一系列示例。
2021-08-25 cs.PL
Finite Functional Programming
University of California, Berkeley（加州大学伯克利分校）
本文提出有限函数编程，通过将谓词视为具有有限支持的函数，统一了函数式和逻辑编程，用于处理聚合和加权逻辑编程。
2026-04-28 cs.PL
Language Support for Declarative Future Commitments
顺序编程和工作流编程是描述计算处理的两种有用但完全不同的方法。在这两者中，顺序编程是我们教给所有程序员的，并得到程序设计语言的支持，无论是过程式的、面向对象的还是函数式的。我们将工作流作为问题分解的次要样式，用于特殊情况，如分布式或网络处理。这两种风格提供了互补的优势，但事实上，它们采用了完全不同的延续所有权模型，这妨碍了我们以一种允许在单一程序设计语言中教授和使用它们的方式将它们集成的能力。本文介绍了一种程序设计语言构造，声明性的未来承诺，允许更好地集成两者。
2011-08-23 cs.PL
Context-Oriented Programming: A Programming Paradigm for Autonomic Systems
动态软件适应性是自主计算所利用的核心特性之一。然而，开发在运行时间改变其行为以适应操作条件的软件是一项具有挑战性的任务。在文献中已经提出了几种方法来解决这个问题，在不同的和互补的抽象层次：软件体系结构，中间件和编程水平。我们专注于ad-hoc程序设计语言结构可能提供的支持，以支持动态自适应行为。我们介绍了面向上下文的程序设计语言，我们提出了一个框架，该框架的位置在MAPE-K自主循环支持的范例。我们讨论了使用面向上下文的程序设计语言，而不是其他主流方法的基础上，面向动态方面的程序设计语言的优势，并提出了一个案例研究，显示如何提出的编程风格自然适合动态适应的要求。最后，我们讨论了一些已知的问题，并概述了一些开放的研究挑战。
2012-03-30 cs.PL
Logic programming in the context of multiparadigm programming: the Oz experience
Oz是一种多范式语言，支持逻辑编程作为其主要范式之一。多范式语言被设计为支持不同的编程范式（逻辑、函数、约束、面向对象、顺序、并发等）。同样轻松。本文有两个目标：在Oz中给出逻辑编程的教程，并展示逻辑编程如何自然地融入多范式编程的更广泛背景。我们的经验表明，有两类问题，我们称之为算法和搜索问题，逻辑编程可以帮助制定实际的解决方案。数学问题有已知的有效算法。搜索问题没有已知的有效算法，但可以用搜索来解决。Oz对逻辑编程的支持专门针对这两个问题类，使用每个问题类所需的概念。这与Prolog方法相反，Prolog方法用一组概念来针对两个类，这导致对每个类的支持不是最佳的。为了解释算法程序和搜索程序之间的本质区别，我们定义了Oz执行模型。这个模型包含了并发逻辑编程（committed-choice-style）和基于搜索的逻辑编程（Prolog-style）。与Horn子句语法不同，Oz有一个简单的、完全组合的、高阶的语法，它适应了语言的能力。最后，我们总结了从这项工作中吸取的教训，奥兹国的简史，以及奥兹国文学的许多切入点。
2002-08-20 cs.PL
Gradual Certified Programming in Coq
表达性的静态类型规则是实现高质量软件的一种强有力的方法。然而，不应低估采用这些技术的成本。就像渐进式类型允许从动态类型到静态类型的程序的平滑过渡一样，支持渐进式路径到认证编程似乎是可取的。我们探索逐步认证的编程在Coq，提供了可能性，推迟选定的属性的证明，并检查“在运行时”是否属性实际上举行。强制转换可以与Coq的隐式强制机制集成，以支持隐式强制转换插入（渐进类型化）。此外，当将Coq函数提取到主流语言时，我们的强制转换编码支持将假定的属性提升到运行时检查中。令我们惊讶的是，没有必要以任何方式扩展Coq来支持渐进式认证编程。类型类和公理的简单混合使得以简单的方式将渐进认证编程引入Coq成为可能。
2015-08-22 cs.PL
Categorical Message Passing Language (CaMPL) for programmers
Universidade Federal do Rio de Janeiro（里约热内卢联邦大学）；University of Calgary（卡尔加里大学）；Tallinn University of Technology（塔林科技大学）
CaMPL是一种基于范畴论的并发编程语言，通过类型通信通道实现消息传递，支持受控非确定性、高阶过程和自定义通道类型，确保程序不会死锁或活锁。
2026-05-10 cs.DC cs.LO cs.PL
OESPA:A Theory of Programming that Support Software Engineering
提出了一种新的规划理论。该理论由操作表达式（OE）、语义谓词（SP）和公理（A）组成，简称OESPA。OE用于编程：它的语法由BNF公式给出，它的语义由这些公式上的公理定义。与逻辑中的谓词类似，SP用于描述OE（即程序）的属性和程序属性分析。但SP与谓词不同，它直接将给定OE终止时变量的最终值与同一OE之前这些变量的初始值联系起来，因此可以通过基于A（Axioms）的计算来证明或反驳给定SP是否是给定OE的属性。SP演算是为解决软件工程中缺少的程序规格说明和规格说明分析问题而提出的。
2013-04-02 cs.PL
Language Support for Adaptation: Intent-Driven Programming in FAST
从历史上看，程序设计语言语义集中于为程序分配精确的数学含义。这个意义是一个从程序的输入域到输出域的函数，它完全由程序的句法结构决定。这样的语义促进了便携式应用的开发，该便携式应用不注意特定硬件和软件平台的性能特性和限制（诸如最大存储器占用）。本文介绍了意图驱动编程的思想，其中程序的含义还取决于一个附带的意图规范，表示如何在执行过程中动态修改普通程序的含义，以满足意图所表达的附加属性。这些包括两种内涵属性-例如，资源使用-和扩展属性-例如，计算答案的准确性。为了证明意图驱动编程模型的价值，本文提出了一种通用意图驱动的程序设计语言--称为FAST--作为Swift的扩展实现。FAST由一个意图编译器、一个分析器、一个通用控制器接口和一个运行时模块组成，该模块支持与传统C/C++代码的互操作。与现有的自适应计算框架相比，\FAST{}支持对操作环境和意图本身的变化进行动态适应，并支持混合过程控制和基于反馈和优化的控制。
2019-07-12 cs.PL
Design Patterns for Functional Strategic Programming
在以前的工作中，我们介绍了\emph{strategic programming}的基础知识和支持组合子库。这是一种基于\emph{functional strategy}概念的泛型编程习惯用法：一种第一类泛型函数，不仅可以应用于任何类型的项，而且还允许泛型遍历到子项，并可以使用特定于类型的行为进行定制。本文旨在为实践功能程序员提供实用的指导，在制定自己的战略计划。我们从用户的角度介绍基本原理和支持，并启动\emph{strategy design patterns}目录。这些设计模式旨在以可访问的形式巩固战略编程专业知识。
2002-04-09 cs.PL
A Functional Programming Language with Versions
虽然现代软件开发大量使用版本化包，但程序设计语言很少在其语义中支持版本的概念，这使得软件更新更加庞大和不安全。本文提出了一种本质上支持版本的程序设计语言。其主要目标是设计核心语言功能，以支持在一个程序中的多个版本，并建立一个适当的概念，类型安全与这些功能。所提出的核心演算称为Lambda VL，具有版本化的值，每个值在不同版本下包含不同的值。我们的类型系统的建设作为一个扩展的coeffect演算的版本映射到计算资源。类型系统保证程序存在有效的版本组合。演算使程序设计语言能够在程序中使用包的多个版本。它将作为设计高级语言功能（如模块系统和语义版本）的基础。
2021-07-15 cs.PL
Eliom: A Language for Modular Tierless Web Programming
分层Web程序设计语言允许程序员在单个程序中组合客户端和服务器端编程。这样，程序员就可以用客户端和服务器端来定义组件，并获得灵活、高效和类型安全的客户端-服务器通信。然而，在大多数无层次语言中发现的富有表现力的客户端-服务器特性不一定与许多主流语言中发现的功能兼容。特别是，我们希望受益于类型安全，高效执行，静态编译，模块化和单独编译。在本文中，我们提出了Eliom，一个工业强度的无层次功能的Web程序设计语言，扩展OCaml支持丰富的客户端/服务器交互。它允许将整个应用程序构建为单个分布式程序，其中可以定义具有服务器和客户端行为的模块化无分层库，并毫不费力地将它们组合在一起。Eliom是唯一一种将类型安全和高效的客户端/服务器通信与支持单独编译和模块化的静态编译模型相结合的语言。它还支持与OCaml的出色集成，允许透明地利用其生态系统。为了实现所有这些功能，Eliom不仅借鉴了分布式程序设计语言的思想，还借鉴了元编程和现代模块系统的思想。我们提出了Eliom的设计，它如何在实践中使用和它的形式化，包括它的类型系统，语义和编译方案。我们表明，这种编译方案保留类型和语义，它支持单独的编译。
2019-01-31 cs.PL
typedKanren: Statically Typed Relational Programming with Exhaustive Matching in Haskell
本文提出在Haskell中静态类型嵌入带不等性约束的miniKanren关系编程，通过支持静态穷尽性检查的关系匹配扩展组合子库，并利用GHC.Generics与Template Haskell简化用户自定义类型的逻辑编程，最后以示例验证并比较性能。
2024-08-30 cs.PL
Programming with Algebraic Effects and Handlers
Eff是一种基于计算效果的代数方法的程序设计语言，其中效果被视为代数运算，效果处理程序被视为自由代数的同态。Eff支持一流的效果和处理程序，通过它们，我们可以轻松定义新的计算效果，无缝地组合现有的效果，并以新颖的方式处理它们。我们给出了一个指称语义的EFF和讨论的原型实现的基础上，通过例子，我们演示了如何在EFF的标准效果处理，以及如何EFF支持编程技术，使用各种形式的定界延续，如回溯，广度优先搜索，选择功能，合作多线程，和其他。
2012-03-07 cs.PL
A Survey on Hardware and Software Support for Thread Level Parallelism
为了支持不断增长的大规模并行性，功能组件以及当前处理器的能力正在改变并继续这样做。当今的计算机构建在多个处理核心上，运行由大量线程组成的应用程序，这使得运行时线程管理成为一个复杂的过程。此外，每个核可以支持多个并发线程执行。因此，硬件和软件支持线程是越来越需要提高峰值性能容量，整体系统吞吐量，因此一直是许多研究的主题。本文调查，许多建议或目前可用的解决方案，执行，分布和管理线程的硬件和软件。当前应用的性质是多种多样的。为了提高系统性能，并不是所有的编程模型都适合利用多核处理器内置的大规模并行性。由于硬件的异构性，混合编程模型（它结合了共享和分布式模型的特点）目前已成为非常有前途的。在本文中，首先，我们已经给出了一个概述线程，线程机制及其在执行过程中的管理问题。接下来，我们讨论了不同的并行编程模型，考虑到他们的显式线程支持。我们还回顾了编程模型对共享内存，分布式内存和异构性的支持。执行时的硬件支持对系统的性能非常关键，因此也存在或已经提出了不同类型的线程硬件支持，主要基于广泛使用的编程模型。我们还进一步讨论了软件对线程的支持，主要是增加运行时的确定性行为。最后，我们通过讨论与线程管理相关的一些常见问题来总结本文。
2016-04-06 cs.PL
Distributed Reactive Programming for Reactive Distributed Systems
上下文：术语反应性在两个研究领域很流行：程序设计语言和分布式系统。一方面，反应式编程是一种范式，它为程序员提供了以声明方式编写事件驱动应用程序的方法。另一方面，反应式分布式系统以及时的方式处理客户端请求，而不管负载或故障。查询：响应式程序设计语言和框架的实现分布式系统之前已经提出。然而，我们认为，这些方法是不适合实现反应式分布式系统。方法：我们分析了分布式反应式编程的最先进的运行时，并确定了两个关键问题的反应式分布式系统。它们依赖于单一的中心协调点和/或假设它们所支持的系统中没有部分故障。知识：基于我们的分析，我们提出了一个新的分布式反应式程序设计语言和框架的运行时。这个运行时在设计上支持反应式分布式系统。基础：我们在JavaScript中实现了一个用于反应式分布式系统的概念验证框架，该框架构建在我们的运行时之上。使用这个框架，我们实现了一个案例研究应用程序，突出了我们的方法的适用性。此外，我们基准我们的运行时对类似的方法，以展示其运行时属性，我们证明了它的正确性。重要性：这项工作旨在弥合两种反应之间的差距：反应式分布式系统和分布式反应式编程。当前的分布式反应式编程方法不支持反应式分布式系统。我们的运行时是第一个弥合这种反应性差距的：它允许使用分布式反应式编程实现反应式分布式系统。
2019-02-01 cs.PL
A Constraint and Object Oriented Fifth Generation Programming Language and its Compiler and Runtime System
自LISP语言问世以来，第五代程序设计语言已经发展了几十年。然而，与第四代程序设计语言相比，第五代程序设计语言由于语义晦涩、问题表示严谨、推理能力有限等原因，一直没有得到广泛应用。为此，本文提出的第五代程序设计语言COOL（Constraint and Object Ordered Language）克服了以往第五代程序设计语言语义直观、处理问题条件限制严格等问题，提高了其推理能力。具体改进如下：第一，COOL支持面向过程和面向对象，便于在生产项目中应用;第二，COOL支持表达式作为函数声明和函数返回，提高了对数学公式的语言亲和力，支持将函数参数嵌入函数名字符串，使函数命名更接近自然语言。使数学问题更容易描述;第三，COOL引入了加权机制，通过累积加权加速推理过程。第四，COOL在编程中引入了正向和反向函数的概念，这样计算机就可以推断和执行具有逻辑顺序约束的问题。第五，计算机可以通过回溯算法和动态规划算法，利用正解过程推导出逆解过程，从而使计算机能够推导出具有时序约束的问题。第六，引入预执行步骤，将程序的推理和函数查询过程与执行过程分离，提高程序的执行速度。
2022-06-02 cs.PL
Adaptation-Based Programming in Haskell
我们提出了一个嵌入式DSL，以支持基于自适应编程（ABP）在Haskell。ABP是一个抽象的模型，用于定义自适应值，称为自适应值，它根据一些相关的反馈进行调整。我们展示了我们在Haskell中的设计选择如何激励更高级别的组合子和构造，并帮助我们获得更复杂的组合自适应。我们还展示了ABP的一个重要专业化是支持强化学习结构，它根据程序员指定的目标函数优化自适应值。这使得ABP用户可以轻松地定义自适应值，以表达其程序中任何地方的不确定性。在重复执行过程中，这些自适应值会调整为更有效的值，并使用户的程序能够自我优化。我们的DSL的设计很大程度上依赖于类型类的使用。在介绍DSL的同时，我们还将举例说明类型类的使用如何支持DSL的逐步发展。
2011-09-05 cs.PL
Traits for Correct-by-Construction Programming
我们证明，性状是一种自然的方式来支持正确的建设（CbC）在现有的程序设计语言在传统的事后验证（PhV）的存在。通过构造正确性，程序是随着内在保证满足的规范而递增地构造的。在没有专门工具支持的情况下使用CbC是复杂的，因为它需要一组固定粒度的细化规则，这些规则是程序设计语言之上的附加规则。在这项工作中，我们提出了TraitCbC，一个增量的程序建设过程，实现正确的基础上，通过使用性状的PhV建设。TraitCbC允许通过特征组合而不是细化规则来构建程序。它提供了一个编程指南，类似于CbC应该导致结构良好的程序，并允许灵活地重用已验证的程序构建块。我们正式介绍TraitCbC和证明我们的验证策略的合理性。此外，我们实现TraitCbC作为概念验证。
2022-04-12 cs.PL
Lazy Stream Programming in Prolog
近年来，流处理已经成为增量处理大量数据的重要方法，在许多程序设计语言中有特殊的支持和库。不幸的是，到目前为止，Prolog中的支持还很缺乏，而且大多数现有的方法都是临时的。为了解决这种情况，我们提出懒惰流生成器作为一个统一的Prolog接口，用于通过I/O和/或算法增量产生的有限和无限数据序列的有状态计算。我们以两种方式向应用程序员公开流生成器：1）通过抽象序列操作API，便于定义自定义生成器，2）作为惯用的惰性列表，与许多现有的列表谓词兼容。我们定义了一个代数的流生成器操作，扩展Prolog通过嵌入式语言解释器，提供了一个紧凑的符号组成的发电机和支持移动之间的两个同构表示。作为一个特殊的例子，我们介绍了答案流生成器，封装协同编程一流的逻辑引擎的工作，并支持前向递归与流和回溯生成的或流之间的互操作。关键词：惰性流生成器，惰性列表，第一类逻辑引擎，流组合器，与流/或流互操作，Prolog扩展
2019-09-19 cs.PL
Generic Programming with Combinators and Objects
我们提出了一个通用的编程框架OCAML，它使得有可能实现可扩展的转换为大规模的类型定义。我们的框架利用OCAML的面向对象的功能，利用后期绑定覆盖生成的转换的默认行为。对多态变体类型的支持补充了描述可组合数据类型的能力和实现可组合转换的能力。
2021-06-02 cs.PL
Efficient lambda encodings for Mendler-style coinductive types in Cedille
在依赖lambda消除演算（CDLE）中，可以通过lambda编码来定义归纳数据集，该编码具有常数时间析构函数和值过程归纳方案。本文首先讨论了对偶共归纳类型的缺失导子。我们的推导利用CDLE内的新方法，因为在适应以前已知的方法推导归纳类型似乎有根本的困难。我们提出的实现共归纳类型的lambda编码具有常数时间构造函数和一个值过程共递归方案。还支持共归纳类型族，支持许多标准共归纳属性的证明，例如流互模拟。所有工作都由Cedille工具（CDLE的一个实现）进行机械验证。
2020-05-01 cs.LO cs.PL
Protocol Programming: A Connection of the Digital World
当前的计算机程序设计将属性和行为封装到对象中，但缺少支持对象之间连接的机制。提出了一种连接所有对象的编程范式。连接支持通信。协议被定义为协调对象之间的行为，从而使对象能够跨不同平台进行交互。连接还提供了一种有效的机制来支持并发、并行、分布、流水线和适应性等，它们可以透明地、自治地甚至自适应地进行管理。本文还讨论了协议编程的一个实现，以说明协议编程的有效性。
2016-03-22 cs.PL cs.SE
Programming-By-Example by Programming-By-Example: Synthesis of Looping Programs
程序合成近年来有了许多新的应用，这在很大程度上要归功于SyGuS的引入。然而，现有的SyGuS求解器都不支持合成递归函数。我们介绍了一个多阶段的算法，在SyGuS中的递归“loolike”程序的合成编程的例子。我们单独解决约束，并将其视为递归程序如何行为的“展开”示例，并求解广义递归解。我们的方法是模块化的，支持任何SyGuS求解器。
2021-08-19 cs.LO cs.PL
Theorem proving support in programming language semantics
我们描述了几种观点的语义的一个简单的程序设计语言的正式文件中的演算的归纳结构，可以验证的Coq证明系统。涵盖的方面是自然语义、指称语义、公理语义和抽象解释。递归函数的描述也在适当的时候提供，从而产生一个验证条件生成器和一个静态分析器，可以在定理证明器内运行，用于反射证明。还描述了从指称语义提取解释器。所有不同的方面都被正式证明是合理的自然语义规范。
2007-07-10 cs.LO cs.PL
Effective Extensible Programming: Unleashing Julia on GPUs
GPU和其他加速器是用于加速计算密集型可并行化应用的流行设备。然而，对这些设备进行编程是一项艰巨的任务。编写高效的设备代码是具有挑战性的，并且通常是用低级程序设计语言来完成的。高级语言很少得到支持，或者不与高级语言生态系统的其余部分集成。为了克服这一点，我们提出了编译器的基础设施，有效地增加了对新的硬件或环境的支持，现有的程序设计语言。我们通过在Julia程序设计语言中添加对NVIDIA GPU的支持来评估我们的方法。通过与现有编译器的集成，我们大大降低了实现和维护新编译器的成本，并促进了现有应用程序代码的重用。此外，使用高级Julia程序设计语言可以实现GPU编程的新的动态方法。这大大提高了程序员的工作效率，同时保持与官方NVIDIA CUDA工具包相似的应用程序性能。
2017-12-08 cs.DC cs.PL
An Exercise in Invariant-based Programming with Interactive and Automatic Theorem Prover Support
基于不变式的编程（IBP）是一种基于结构的正确的编程方法，其中程序是围绕不变式构建的，这些不变式在实际代码之前被另外制定。Socos是一个专门为支持IBP而构建的程序构建和验证环境。Socos的前端是一个图形化的图表编辑器，允许程序员构建基于不变式的程序并检查其正确性。Socos的后端组件，程序检查器，计算程序的验证条件，并试图自动证明它们。它使用定理证明器PVS和SMT求解器Yices来尽可能多地释放验证条件，而无需用户交互。在本文中，我们首先从用户和系统级的角度描述了Socos环境，然后通过在Socos中构建一个经过验证的堆排序实现来验证IBP工作流。案例研究突出了自动和交互式定理证明在IBP工作流程的三个连续阶段的作用：开发的背景理论，制定程序规范和不变量，并证明最终实现的正确性。
2012-02-22 cs.LO cs.PL
Concept-Based Generic Programming in C++
本文通过示例展示 C++ 中基于概念（Concept）的泛型编程技术，强调其作为语言核心部分的实用性，并阐述概念设计的关键理由与起源。
2025-10-09 cs.PL cs.SE
Towards Distributed Logic Programming based on Computability Logic
DongA University（东亚大学）
{ \em Computability logic}（CoL）是一个强大的计算模型，它将计算问题视为机器及其环境之间的博弈。在本文中，我们表明，CoL自然支持分布式控制的多智能体编程模型。具体地说，我们讨论了一个基于CoL的分布式逻辑编程模型（确切地说是CL 1），我们称之为CL 1 ^Ω。该模型的主要特点是支持Agent的$dynamic/evolving$知识库。事实证明，这种模型是实现通用AI和未来计算模型的一种有前途的方法。
2022-08-07 cs.AI cs.PL
Lupa: A Framework for Large Scale Analysis of the Programming Language Usage
在本文中，我们提出了Lupa -一个大规模分析的程序设计语言的使用框架。Lupa是一个命令行工具，它使用了IntelliJ平台的强大功能，这使它能够访问现代IDE中使用的强大静态分析工具。该工具支持自定义分析器，可以处理代码的丰富具体语法树，并可以计算其各种功能：实体的存在，它们的依赖关系，定义使用链等。我们解释了该工具的内部原理，展示了如何扩展和自定义它，并描述了我们在它的帮助下进行的示例分析：分析Kotlin中范围的语法。
2022-03-28 cs.PL cs.SE
An Integrated Development Environment for Declarative Multi-Paradigm Programming
在本文中，我们提出了CIDER（咖喱集成开发环境），一个分析和编程环境的声明性多范式语言咖喱。CIDER是一个图形环境，通过提供程序分析和可视化的集成工具来支持Curry程序的开发。CIDER完全在Curry中实现，使用GUI编程（基于Tcl/Tk）和元编程库。我们的环境的一个重要方面是开发环境对其他声明性源语言（例如，Prolog或Haskell）和扩展性w.r.t.新的分析方法。为了支持后一个特性，底层实现语言Curry的惰性求值策略变得非常有用。
2001-11-19 cs.PL cs.SE
