Synchronous Programming with Refinement Types
本文提出 CPS 语言 MARVeLus 的形式化，构建其同步细化类型系统元理论，实现验证与实现在同一语言中的结合，并在真实系统上验证同步程序执行。
2024-09-04 cs.PL
Static Trace-Based Deadlock Analysis for Synchronous Mini-Go
我们考虑的问题，静态死锁检测程序在Go程序设计语言，利用同步通道通信。在我们的分析中，用fork操作符扩展的正则表达式捕获程序的通信行为。从一个简单的标准，特点的痕迹无死锁程序，我们开发了基于自动机的方法来检查死锁自由。该方法的实施和评价与一系列的例子。
2016-09-02 cs.PL
Modular Compilation of a Synchronous Language
同步语言依赖于形式化方法，以一种高效和可重用的方式简化应用程序的开发。形式化方法一直被提倡作为一种提高系统可靠性的手段，特别是那些安全或业务关键的系统。由于状态爆炸、不可判定性等限制，开发自动规格说明和验证工具仍然是困难的。在这项工作中，我们设计了一个新的规范模型的基础上反应同步的方法。然后，我们受益于一个正式的框架，非常适合执行编译和正式的系统验证。在实践中，我们设计并实现了一个专用语言（LE）和它的两个语义：抽象语义帮助我们定义一个程序的行为集，并避免在程序的解释歧义;执行等式语义允许模块化编译程序到软件和硬件目标（C代码，VHDL代码，FPGA综合，观察员）。考虑到关键现实应用程序的两个主要要求，我们的方法是相关的：模块化编译使我们能够处理大型系统，基于模型的方法为我们提供了正式的验证。
2008-01-24 cs.LO cs.PL
Efficient compilation and execution of synchronous programs via type-state programming
针对同步程序编译中状态空间爆炸导致难生成高效可执行文件的问题，提出基于图重写规则的线性时间编译技术，结合C++模板元编程生成类型状态程序，实现了与现有水平相当的编译效率和二进制体积，执行速度提升31%-60%。
2025-08-02 cs.PL
Polychronous Interpretation of Synoptic, a Domain Specific Modeling Language for Embedded Flight-Software
SPaCIFY项目旨在为卫星飞行软件行业带来MDE的进步，倡导建立在名为Synoptic的特定领域建模语言上的自上而下的方法。与以前的实时建模方法（如Statecharts和Simulink）一致，Synoptic的特点是在同步框图和状态机中对应用和控制模块进行分层分解。它的语义是在计算的多线程模型中描述的，这是同步语言Signal的模型。
2010-03-02 cs.PL
Interactive Music and Synchronous Reactive Programming
本文介绍了Skini，一种交互式结构音乐的编程方法和执行环境。有了这个系统，作曲家用HipHop.js同步反应语言编写他的乐谱。然后，他们被执行，或发挥，在现场音乐会，在与观众的互动。该系统旨在帮助作曲家在作品的决定性和与公众互动的非决定性之间找到一个很好的平衡。每一个Skini评分的执行都会产生不同但美学上一致的解释。这部作品在音乐领域提出了许多问题。如何将构图和互动结合起来？当听众影响下一场演奏时，如何控制音乐风格？与生成音乐有什么可能的联系？这些都是Skini系统的重要问题，但它们超出了本文的范围，本文只关注该系统的计算机科学方面。从这个角度来看，主要的问题是如何编程的分数和在哪种语言？通用语言是不合适的，因为它们的基本结构（即，变量、函数、循环等）与表达音乐和音乐约束所需的结构不匹配。我们发现，同步程序设计语言是一个更好的适合，因为它们依赖于时间结构，可以直接用于表示乐谱，因为他们的可塑性，使作曲家很容易实验与艺术的变化，他们的初始分数。本文主要研究分数规划。它揭示了一个作曲家应该遵循的过程，从他的第一个音乐直觉到音乐作品的产生。本文介绍了一些摘录的编程的古典音乐作品，它然后精确地涉及到一个实际的录音。电子音乐和爵士乐的例子也提出了，与音频工件，以证明系统的多功能性。最后，简要介绍了过去的现场音乐会作为一个证据的可行性系统。
2020-06-04 cs.PL
Reactive Probabilistic Programming
同步建模是程序设计语言（如Lustre、Esterel或Scade）的核心，通常用于实现安全关键控制软件，例如，飞机的电传操纵和发动机控制。然而，到目前为止，这些语言对建模不确定性（软件环境或行为的概率方面）的现代支持有限，尽管建模不确定性是设计控制系统时的主要活动。在本文中，我们提出了第一个同步概率程序设计语言ProbZelus。ProbZelus保守地提供了编写控制软件的同步语言的设施，具有概率结构来建模不确定性并执行循环中的推理。我们提出的语言的设计和实现。我们提出了概率流函数的测度论语义和一个简单的类型纪律来分离确定性和概率表达式。我们展示了一个语义保持编译成一个一阶函数语言，适合于一个简单的演示推理算法的流模型。我们还重新设计了延迟采样推理算法，以提供高效的流式推理。结合对几个反应式应用程序的评估，我们的结果表明，ProbZelus可以设计反应式概率应用程序和高效的有界内存推理。
2020-04-09 cs.PL
Timetide: A programming model for logically synchronous distributed systems
本文提出编程模型 Timetide，通过多时钟语义和逻辑同步模型实现分布式确定性编程，无需物理时钟同步，并支持形式化验证。
2025-07-19 cs.DC cs.PL
Density-Based Semantics for Reactive Probabilistic Programming
针对概率同步语言仅对已调度方程定义语义的局限，提出两种与调度无关的基于密度函数流的语义（共迭代与关系语义），并利用关系语义证明了状态空间模型优化推理所需程序变换的正确性。
2023-09-07 cs.PL
Tempo: Reconstructing Synchronous Reactive Programming with OCaml 5 Effects
Univ. Orléans, INSA Centre Val de Loire, LIFO UR 4022（奥尔良大学，中央卢瓦尔河谷国立应用科学学院，LIFO UR 4022）
研究能否在普通OCaml 5内重构同步响应式编程核心机制，提出基于代数效果和深度处理程序的Tempo库运行时，通过效果操作界定暂停点、处理程序具体化延续为任务，比较研究量化其开销并确定主导成本的运行时机制。
2026-07-28 cs.LO cs.PL
Rewriting Logic Semantics of a Plan Execution Language
计划执行交换语言（英语：Plan Execution Interchange Language，缩写：PLEXIL）是一种由NASA开发的同步语言，用于支持自主航天器操作。在本文中，我们提出了一个重写的逻辑语义PLEXIL在Maude，一个高性能的逻辑引擎。重写逻辑语义本身就是语言的形式解释器，可以用作PLEXIL执行程序实现的语义基准。在Maude中的实施还有一个额外的好处，即为PLEXIL设计人员和开发人员提供Maude提供的所有正式分析和验证工具。PLEXIL语义在重写逻辑中的形式化提出了一个有趣的挑战，由于语言的同步性和定义其语义的优先级规则。为了克服这个困难，我们提出了一个通用的程序，用于模拟同步集关系重写逻辑是健全的，确定性的关系，完成。我们还报告了两个问题，在设计层面上的原始PLEXIL语义确定的帮助下，在Maude的可执行规范。
2010-02-15 cs.LO cs.PL
Conjure Revisited: Towards Automated Constraint Modelling
University of St Andrews（圣安德鲁斯大学）；University of York（约克大学）；Izmir University of Economics（伊兹密尔经济大学）
约束建模过程的自动化是约束领域面临的主要挑战之一，也是阻碍约束求解广泛采用的主要障碍之一。本文重点介绍了基于细化的自动建模方法，用户指定一个问题的抽象约束规约语言，然后自动细化到一个约束模型。特别是，我们重新审视了2005年首次以原型形式出现的Conjure系统，并提出了一个新的实现，该实现对规约语言Essence的覆盖范围要大得多。
2011-09-08 cs.AI cs.PL
A unified framework for modeling and implementation of hybrid systems with synchronous controllers
University of Auckland（奥克兰大学）
本文提出了一种新的方法，用于在线性混合自动机方法中包含非即时的离散控制转换。通过扩展同步子集的SystemJ编程语言，研究了如何用同步编程语言控制持续变化的模拟植物，并提供了一种合理的重写语义来近似连续变量在离散域中的演化。
2015-01-23 cs.PL cs.SY eess.SY
Precise subtyping for synchronous multiparty sessions
子类型的概念在理论和应用领域都有重要的作用：在lambda和并发演算以及程序设计语言中。健全性和完整性，一起被称为子类型的精确性，可以从两个不同的角度来考虑：操作和指称。前一种精确性最近在类型安全方面得到了发展，即当一个更大类型的项被期望时，一个更小类型的项的安全替换。后者的精确性是基于一个类型的外延，这是一个数学对象，它根据语言中其他表达式的外延来描述该类型的含义。本文的结果是一个同步多方会话演算的子类型的操作和指称的精确性。本文的创新之处在于引入了特征全局类型来证明运算完备性。
2016-02-11 cs.LO cs.PL
Correctly Implementing Synchronous Message Passing in the Pi-Calculus By Concurrent Haskell's MVars
并发程序设计语言的比较和并发环境下程序转换的正确性是本文研究的重点。作为标准，我们使用的上下文语义适应并发，在那里可能-以及应该-收敛观察。本文研究了并发Haskell（CH）核心语言与同步π演算的关系。上下文语义一方面对操作语义的细节给予宽容，另一方面对翻译后过程之间的相互作用提出了强烈的要求。我们的结果是，CH包含同步π演算。我们的主要任务是通过CH的并发原语（MVars）来发现和证明π演算通道编码的正确性。它们的行为类似于（阻塞）1位缓冲区，对共享内存进行建模。第一个开发的翻译使用一个额外的私人MVar的每一个通信。我们还自动生成和检查潜在的正确的翻译，重用MVar，其中一个MVar包含的消息和两个额外的MVar同步用于模拟一个通道的同步通信的pi演算。我们的自动实验结果导致推测，一个额外的MVar是不够的。
2020-08-31 cs.LO cs.PL
In the Age of Web: Typed Functional-First Programming Revisited
大多数程序设计语言都是在网络时代之前设计的。这很重要，因为web改变了许多类型函数式语言设计者认为理所当然的假设。例如，程序不能在封闭的世界中运行，而是必须与（不断变化且可能不可靠的）服务和数据源交互，通信通常是异步的或事件驱动的，程序需要与非类型化环境进行互操作。在本文中，我们介绍了F#语言和库如何面对Web带来的挑战。从技术上讲，这包括使用类型提供程序来与外部信息源集成以及与非类型化编程环境集成，使用轻量级元编程来针对JavaScript和计算表达式来编写异步代码。在这个调查中，整体的观点比孤立的每个特征更重要。我们使用一个实际的案例研究作为起点，看看F#语言和库如何应对Web带来的挑战。具体的经验教训可能不如我们试图揭示在网络时代不再成立的隐藏假设那么有趣。
2015-12-07 cs.PL cs.SE
LoKit (revisited): A Toolkit for Building Distributed Collaborative Applications
本文介绍了基于协调语言LO的分布式协作应用构建工具包LoKit，阐述其概念与部分工具，并通过示例应用验证了该工具包的实用价值。
2023-12-19 cs.PL cs.SC
Interleaving classical and reversible
给定一个简单的递归函数，我们展示了如何提取两个相互作用的进程，这两个进程可以通过迭代程序来描述，其中一个是本质上可逆的，在一种语言中，直到微小的细节，属于广泛使用的命令式程序设计语言的核心。我们实现的两个进程交错同步JAVA线程的相互作用是等效的递归函数，他们从中提取。
2021-02-18 cs.PL
Orthogonal Persistence Revisited
潜在的长期存在的大量程序和数据的社会和经济重要性已经引起了商业和研究界的广泛关注。在这里，我们集中讨论一组称为持久编程的方法和技术。特别是，我们审查程序设计语言支持的概念，正交持久性，一种技术的对象的统一处理，无论其类型或寿命。虽然持久性编程的研究已经变得不流行，我们展示了这个概念是如何开始出现作为现代系统的一个主要组成部分。我们将这些尝试与正交持久性的原始原理联系起来，并给出了一些关于未来如何利用这一概念的提示。
2010-06-17 cs.DB cs.PL
A Case for Stale Synchronous Distributed Model for Declarative Recursive Computation
一旦递归中允许聚合，一大类传统的图和数据采掘算法可以用Datasheet和其他基于逻辑的语言简洁地表达。事实上，对于大多数BigData算法，在递归中使用非单调聚合所带来的困难语义问题通过Pre-Mappability（PreM）解决，PreM是一种属性，可以确保对于递归中使用聚合的程序，存在等效的聚合分层程序。在本文中，我们表明，通过将分层程序的形式抽象语义与非分层程序的有效操作语义结合在一起，PreM也可以促进和提高它们的并行执行。我们证明了PreM优化的无锁和可分解的并行半天真评价产生相同的结果作为单一的执行器程序。因此，PreM可以被同化到不同的分布式系统的数据并行计算计划，无论这些是否遵循批量同步并行（BSP）或异步计算模型。此外，我们表明，非线性递归查询可以使用混合陈旧的同步并行（SSP）模型在分布式环境中进行评估。在提供了一个正式的正确性证明的递归查询评估与PreM在这个宽松的同步模型下，我们提出了实验证据，其好处。本文正在考虑接受逻辑编程理论与实践（TPLP）。
2019-07-24 cs.DB cs.DC cs.LO
LFPL: Revisited and Mechanized
Carnegie Mellon University（卡内基梅隆大学）
本文重新审视并机械化了LFPL语言及其元理论，提供自包含且易懂的现代描述，简化了已知最强的正确性与完备性结果。
2026-07-10 cs.CC cs.LO cs.PL
