A denotationally-based program logic for higher-order store
本文提出了一种基于指称语义的高阶分离逻辑TULIP，用于System F{mu,ref}，通过等式重写简化了传统操作语义下的纯证明步骤，并证明了其可靠性。
2023-11-17 cs.LO cs.PL
Towards a Denotational Semantics for Proofs in Constructive Modal Logic
本文给出了构造模态逻辑CK和CD中证明的两种新语义。第一个语义是通过扩展命题直觉逻辑的组合证明的语法给出的，其中证明被分解为线性片段（竞技场网）和并行的弱化收缩片段（斜纤维化）。特别是，我们提供了一个编码的模态公式通过有向图（模态竞技场），和一个编码的线性证明作为模态竞技场配备满足拓扑标准的顶点分区。第二个语义是通过赢得无辜的策略，两个球员的游戏模式舞台。这是通过在Hyland-Ong竞技场中扩展直觉组合证明和获胜无辜策略之间的Heijltjes-Hughes-Straßburger对应关系给出的。使用我们的第一个结果，我们提供了一个表征的获胜策略的游戏模式舞台上对应的模态证明。
2021-04-19 cs.LO math.LO
Universal Semantics for the Stochastic Lambda-Calculus
我们为随机λ演算定义了合理的和充分的指称和操作语义。这两种语义方法建立在以前的工作，使用类似的技术来推理高阶概率程序，但第一次承认一个充分性定理有关的操作和指称的意见。这解决了（Bacci等人，2018）中未解决的主要问题。
2021-05-14 cs.LO
Domain Theory and the Logic of Observable Properties
斯通对偶的数学框架被用来合成理论计算机科学中迄今为止独立的一些发展：域理论，斯科特作为指称语义的基础引入的计算数学理论。- Milner、Hennessy等人基于操作语义提出的并发性和系统行为理论。- 程序的逻辑。斯通对偶提供了语义（点的空间=计算过程的表示）和逻辑（过程的属性格）之间的连接。此外，底层逻辑是几何的，它可以在计算上被解释为可观察属性的逻辑-即可以根据关于其执行的有限数量的信息来确定过程的属性。这些想法导致以下方案：1.元语言的介绍，包括-类型=宇宙的话语各种计算的情况。- 术语=程序=模型或点的语法内涵。2.一个标准的指称解释的元语言，分配域的类型和域元素的条款。3.元语言也给出了{ \em逻辑}解释，其中类型被解释为命题理论，术语通过程序逻辑解释，该程序逻辑将它们满足的属性公理化。4.这两种解释是相互关联的，表明它们是彼此的石头。因此，语义学和逻辑学保证了彼此的和谐，事实上，每一个都决定着另一个，直到同构。这为一系列应用开辟了道路。在我们的元语言中，给定一个计算情形的指称描述，我们可以转动句柄来获得该情形的逻辑。
2011-12-01 cs.LO
Categorical models of Linear Logic with fixed points of formulas
我们开发了一个指称语义的muLL，一个版本的命题线性逻辑与最小和最大的不动点扩展大卫Baelde的命题muMALL与指数。我们的一般范畴设置是基于西利范畴的概念和强函子作用于他们。我们展示两个简单的例子，这种设置。在第一个，这是基于类别的集合和关系，最小和最大的不动点是以同样的方式解释。在第二种情况下，基于一个配备了总体概念（非一致总体空间）和保持它们的关系的集合范畴，最小和最大不动点有不同的解释。后一个模型表明，muLL享有一个指称形式的规范化证明。
2021-05-19 cs.LO
Execution Time of lambda-Terms via Denotational Semantics and Intersection Types
线性逻辑的基于多集的关系模型导出了无类型演算的语义，它对应于一个非幂等交类型系统System R。我们证明了，在系统R中，类型派生的大小和类型的大小是密切相关的执行时间在一个特定的环境机器，Krivine的机器。
2009-05-26 cs.CC cs.LO
Modular Denotational Semantics for Effects with Guarded Interaction Trees
本文提出受守卫的交互树及其配套分离逻辑，用于在Coq中表示带高阶效应的高阶计算，并证明了类PCF语言解释的可靠性与计算充分性，同时实现了不同效应的模块化组合与跨语言安全互操作。
2023-11-20 cs.LO cs.PL
Denotational Semantics of the Simplified Lambda-Mu Calculus and a New Deduction System of Classical Type Theory
经典（或布尔）类型论是允许类型推断$σ\to \bot) \to \bot => σ$（双重否定消除的类型对应物）的类型论，其中$σ$是任何类型，$\bot$是荒谬类型。本文首先提出了一个指称语义的简化版本的Parigot的Alzoda-mu演算，经典的类型论的一个重要例子。在这种语义中，每个类型的定义域被划分为无限多个等级，不仅包含等级为0的类型的通常成员，还包含它们在更高等级中的否定、合取和析取阴影，这形成了一个无限嵌套的布尔结构。荒谬类型$\bot$被识别为真值类型。然后，本文提出了一个新的演绎系统的经典类型论，一个演算称为经典类型系统（CTS），它涉及到标准的逻辑运算符，如否定，合取，和分离，从而反映了讨论的语义结构，在一个更直接的方式。
2016-06-21 cs.LO
Revisiting Elementary Denotational Semantics
操作语义已经取得了巨大的成功，这在很大程度上是由于它的灵活性和简单性，但它们不是组合的。另一方面，指称语义是组合的，但格理论模型很复杂，难以扩展到大型语言。然而，也有简单得多的$λ$ -演算的基本模型：Coppo、Dezani-Ciancaglini和Salle（1979）、Engeler（1981）和Plotkin（1993）。本文采取的第一步回答这个问题：可以基本模型是好的语言规范，机械化和编译器的正确性的日常工作？文献中的基本模型很简单，但它们并不像它们所能做到的那样直观。为了解决这个问题，我们创建了一个新的模型，将函数字面上表示为有限图。关于机械化，我们给出了第一个机器检查证明的合理性和完整性的基本模型相对于一个操作语义。关于编译器的正确性，我们定义了一个多变量内联调用的值$λ$ -演算，并证明其输出是上下文等价于其输入。为了将基本模型扩展到更大的语言，我们用一元风格制定我们的语义，给出了具有一般递归的系统F的语义，并机械化类型可靠性的证明。
2017-10-21 cs.LO cs.PL
Weak topologies for Linear Logic
本文构造了线性逻辑的一个指称模型，其对象是所有局部凸的、可分离的拓扑向量空间，并赋予它们弱拓扑。否定被解释为对偶，线性证明被解释为连续线性函数，非线性证明被解释为单项式序列。我们并不是通过双正交运算来完成我们的构造。这就产生了一种从拓扑学角度对连接词极性的解释。
2016-03-07 cs.LO
Denotational semantics of general store and polymorphism
本文首次提出结合卫递归与非直谓多态性的多态依赖类型理论指称语义，支持一般高阶引用和递归类型，并通过“逻辑关系即类型”的模态构造实现对有状态抽象数据类型的关系推理。
2023-04-12 cs.LO cs.PL
Denotational semantics for stabiliser quantum programs
University of Oxford（牛津大学）；Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, CentraleSupélec, Laboratoire Méthodes Formelles（巴黎萨克雷大学、法国国家科学研究中心、巴黎萨克雷高等师范学院、Inria、中央苏佩莱克学院、形式方法实验室）
本文提出了一种适用于稳定子量子程序的可辨识语义学，通过将操作解释为有限域上的仿射关系，提供了计算上可处理的替代方案，并展示了其在量子纠错中的应用潜力。
2025-11-27 cs.LO math.CT math.SG
IMP with exceptions over decorated logic
在本文中，我们促进不纯的程序设计语言的推理，通过注释术语与“装饰”，描述什么计算（副作用）评估一个术语可能涉及。在一个点自由的范畴语言，称为“装饰逻辑”，我们正式的可变状态和异常的影响，首先分别利用他们之间的anice对偶，然后结合。组合修饰逻辑被用作IMP+Exc命令式程序设计语言的指称语义的目标语言，并允许我们证明用IMP+ Exc编写的程序之间的等价性。
2018-10-16 cs.LO
Formal Semantics of a Classical-Quantum Language
我们调查的形式语义的一个简单的命令式语言，具有经典和量子结构。更具体地说，我们提供了一个操作语义，一个指称语义和两个霍尔风格的证明系统：一个抽象的和一个具体的。这两个证明系统是基于满意度的，灵感来自于Barthe等人的概率程序的程序逻辑。抽象的证明体系是健全的、相对完整的，而具体的证明体系只是健全的。
2021-07-02 cs.LO
Denotational semantics of recursive types in synthetic guarded domain theory
就像数学的任何其他分支一样，程序设计语言的指称语义应该在类型论中形式化，但是将传统的域理论语义（如最初在经典集合论中制定的）适应类型论已经证明是具有挑战性的。本文是一个项目的一部分，制定指称语义的类型论与保护递归。这样做的好处不仅是提供更简单的语义和充分性等属性的证明，而且有望在未来扩展到具有高级功能的语言，如通用引用，超出了传统域理论技术的范围。工作在保护依赖类型论（GDTT），我们开发的指称语义的FPC，简单类型的λ演算扩展与递归类型，建模的递归类型的FPC使用保护递归类型的GDTT。我们证明了GDTT模型的合理性和计算充分性，使用语法和语义之间的逻辑关系，也使用守护递归类型。指称语义是内涵的，在这个意义上，它计算计算一个项的值所需的展开-折叠约简的数量，但是我们构建了一个关系，该关系涉及外延相等项的指称，即，在不同步骤中计算相同值的项对。最后，我们展示了如何在类型论中执行术语的指称语义，并证明了执行布尔术语的指称计算与FPC的操作语义相同的值。
2018-05-02 cs.LO 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
The Denotational Semantics of SSA
该研究提出SSA变体的类型论与范畴语义，证明其可靠完备，给出含TSO弱内存模型的实例，且相关证明已在Lean中机械化，为编译器变换验证提供语义基础。
2024-12-12 cs.LO cs.PL
Denotational semantics driven simplicial homology?
本文探讨由线性逻辑指称语义生成的单纯复形及其同调，并指出为兼容类型同构需在单纯关系上定义同调函子，从而引出单子变换是否保持同调及语义意义的问题。
2024-09-17 cs.LO math.LO
Better Late Than Never: A Fully Abstract Semantics for Classical Processes
我们提出了超经典过程（HCP），这是对线性逻辑和π演算之间的“证明作为过程”对应关系的修订解释，最初由Abramsky [1994]提出，后来由Bellin和Scott [1994]，Caires和Pfenning [2010]以及Wadler [2014]等开发。HCP通过保守地将线性逻辑扩展到hyperenuments（环境的集合，受到Avron [1991]的hypersequences的启发），修补了线性逻辑与π演算中并行组合的语法和可观察语义之间的差异。在hyperenvironments的环境分离是内在的$\otimes$，并对应于并行过程的行为。由于这个属性，我们第一次能够从证明重写中提取标记转换系统（lts）语义。利用类型级别上的并行性信息，我们获得了Merro和Sangiorgi [2004]在π演算中为非阻塞I/O建模而制定的延迟操作的逻辑重构。我们定义了一个基于Brzozowski导数的过程的指称语义，并揭示了HCP中的非干扰对应于Fubini的双重反导定理。有一个lts允许我们使用行为理论的标准工具箱来验证HCP。我们对HCP的双相似性和倒刺同余进行了实例化，得到了一个完整的抽象结果：双相似性、指称等价性和倒刺同余一致。
2018-11-06 cs.LO
Denotational Foundations for Expected Cost Analysis
本文提出基于按值传递调用（CBPV）的元语言 cert，定义代价与期望代价两种指称语义，证明其可靠性、充分性及效应模拟性质，并通过案例展示其表达能力。
2025-02-26 cs.LO cs.PL
DB Category: Denotational Semantics for View-based Database Mappings
我们提出了一个分类的指称语义的数据库映射，视图的基础上，在最一般的框架中的数据库集成/交换。已开发的数据库范畴DB，用于数据库（对象）和它们之间基于视图的映射（态射），与Set范畴不同：态射（基于一组复杂的查询计算）不是函数，而对象是数据库实例（关系集）。数据库之间基于逻辑的模式映射，通常用高度表达性的逻辑语言（例如，LAV、GAV、GLAV映射或元组生成依赖性）可以函数地转换成该“计算”类别DB。采用了一种新的方法，基于数据库的行为的观点，并建立数据库及其映射的行为等价。通过引入基于视图的数据库观测，这是没有副作用的计算，我们定义了一个基本的（泛代数）单子与幂视图endofunctor T。所得到的2-category DB是对称的，因此任何映射也可以表示为对象（数据库实例），其中映射之间的更高级别映射是2-cell态射。数据库类DB具有如下性质：它等于它的对偶、完全和共完全。特别注意实际的例子：一个查询定义，在GAV数据库集成环境中的查询重写，和一个规范的数据集成模型的定点解决方案。
2011-02-24 cs.DB cs.LO math.CT
The stack calculus
我们介绍了一个简单的语法和操作语义的功能演算，其中的演算介绍到目前为止，在Curry-Howard对应的经典逻辑可以忠实地编码。我们的演算没有任何限制地享有汇流。它的类型系统加强了表达式的规范性，是一个健全而完整的全蕴涵经典逻辑系统。我们给出了一个非常简单的指称语义，它可以很容易地计算表达式的解释。
2013-03-29 cs.LO
Revisiting concurrent separation logic
提出了一种基于结构化操作语义（SOS）的并发分离逻辑（CSL）可靠性证明。我们建立在两个以前的证明，并开发新的辅助概念，以实现这一目标。一种使用指称语义（基于跟踪）。另一种是基于SOS，但只针对逻辑的一个片段（Disjoint CSL）获得，它不允许修改并发线程之间的共享变量。在这项工作中，我们解除了这样的限制，证明了健全的充分CSL就SOS。从而有助于开发能够保证实际并发程序正确性的工具。此外，考虑到我们使用SOS，这些工具可以很好地集成到编程环境中，甚至可以合并到编译器中。
2017-12-05 cs.LO
First-order Logic as a Constraint Programming Language
我们提供了一个指称语义的一阶逻辑，捕捉两个级别的视图的计算过程中典型的约束编程。在一个层次上，我们有通常的程序执行。在另一个级别，进行约束存储的自动维护。我们证明，由此产生的语义是健全的真理定义。通过具体形式的约束管理策略的实例化，我们得到了几个良好的评价政策的一阶公式。这种语义也可以用来作为在存在块声明和条件的情况下合理实现约束维护的基础。
2002-11-19 cs.LO
Theorem proving support in programming language semantics
我们描述了几种观点的语义的一个简单的程序设计语言的正式文件中的演算的归纳结构，可以验证的Coq证明系统。涵盖的方面是自然语义、指称语义、公理语义和抽象解释。递归函数的描述也在适当的时候提供，从而产生一个验证条件生成器和一个静态分析器，可以在定理证明器内运行，用于反射证明。还描述了从指称语义提取解释器。所有不同的方面都被正式证明是合理的自然语义规范。
2007-07-10 cs.LO cs.PL
A Sound and Complete Axiomatization of Majority-n Logic
通过多数运算符操纵逻辑函数最近引起了计算机科学研究人员的注意。例如，与传统逻辑系统相比，基于多数运算符的电路优化能够实现更好的结果。此外，布尔可满足性问题发现新的解决方法时，描述的多数决定。为了支持基于多数的计算机逻辑应用，需要一套完善的公理。大多数多数逻辑的最新进展只涉及三元多数（MAJ- 3）运算符，因为只有MAJ-3和互补运算符的公理化是很好理解的。然而，从理论和实践的角度来看，将这样的公理化扩展到n元多数算子（MAJ-n）是很有趣的。在这项工作中，我们解决这个问题，通过引入一个健全的和完整的公理化的MAJ-N逻辑。我们的公理化自然包括现有的多数逻辑系统。基于这组一般公理，计算机应用程序现在可以充分利用多数逻辑的表达能力。
2015-11-25 cs.LO
A Complete Theory of Sequential Digital Circuits: Denotational, Operational and Algebraic Semantics
University of Birmingham（伯明翰大学）；Indiana State University（印第安纳州立大学）
本文通过指称、操作和代数三种语义，为数字电路提供了完备的组合理论，解决了电路自由组合而不需内部细节的问题。
2026-06-26 cs.LO cs.PL math.CT
Denotational Semantics for ODRL: Knowledge-Based Constraint Conflict Detection
RWTH Aachen University, Germany（亚琛工业大学）；Fraunhofer FIT, Sankt Augustin, Germany（弗劳恩霍夫研究所）；University of Galway, Ireland（Galway大学）
本文提出了一种基于知识库的ODRL指称语义，用于解决约束冲突检测问题，通过三种语义领域和三种组合模式，验证了154个基准测试，并证明了冲突的保持性和运行时合理性。
2026-02-23 cs.CL cs.LO
Applying quantitative semantics to higher-order quantum computing
为高阶量子计算寻找一种指称语义是量子程序设计语言语义学中一个长期存在的问题。过去大多数解决这个问题的方法都以这样或那样的方式存在不足，要么将语言限制在一个不可用的小有限片段，要么放弃量子物理学的重要特征，如纠缠。本文利用线性逻辑的定量语义构造了一个具有递归和无限数据类型的量子λ演算的指称语义。
2013-11-10 cs.LO cs.PL quant-ph
Proof Diagrams for Multiplicative Linear Logic: Syntax and Semantics
证明网是线性逻辑证明的一种语法，它给出了关于语法相等的证明等价的粗略概念以及证明的直观几何表示。本文给出了乘法线性逻辑导子的另一种$2$维语法。字符串图的语法授权定义一个框架，其中一个术语的序列化，即决定该术语是否对应于正确的推导，可以在线性时间内验证。此外，我们可以使用这种语法来定义一个指称语义的乘法线性逻辑单元的证明图模的等价类的终止重写。
2017-02-01 cs.LO math.CT
Service-Oriented Logic Programming
我们开发的概念和机制，以支持面向服务的计算正式的基础。我们的工作建立在代数结构（捕获服务编排方式）以及通过所需和所提供服务的逻辑表示形式化服务发现和绑定到给定客户端应用程序的过程中的最新理论进展的基础上。我们展示了如何指称和特定于传统逻辑编程的操作语义可以推广使用的机构理论，以解决静态和动态方面的面向服务的计算。我们的结果依赖于一个强有力的类比之间的发现服务，可以绑定到一个应用程序和搜索一个条款，可以用于计算一个答案的查询;他们探索了对外部服务的请求可以被描述为服务查询的方式，并解释了如何通过统一和解析的面向服务的衍生物来执行其答案的计算，其特征在于服务的绑定和应用的重新配置。
2015-09-02 cs.LO
Semantics, Specification Logic, and Hoare Logic of Exact Real Computation
本文提出精确实数计算语言 ERC，利用 Plotkin 幂域实现可计算且完备的实数语义，并基于可判定的一阶规范逻辑扩展霍尔逻辑，以形式化验证实数程序的完全正确性。
2024-06-21 cs.LO cs.NA math.NA
Sound Conflict Analysis for Timed Contract Automata
针对连续时间下道义规范分析技术的缺失，提出一种可靠但不完备的算法用于检测时间契约自动机中的冲突，证明了其正确性并通过案例研究进行了验证。
2024-10-16 cs.LO
Proof search for propositional abstract separation logics via labelled sequents
分离逻辑是霍尔逻辑的一个扩展族，用于对改变存储器的程序进行推理。这些逻辑是“抽象的”，因为它们独立于任何特定的具体内存模型。他们的断言语言，称为命题抽象分离逻辑，以各种方式扩展了（布尔）集束蕴涵（BBI）逻辑。我们发展了一个模块化的证明理论，各种命题抽象分离逻辑使用割自由标记的代数演算。我们首先扩展了Hou等人的BBI的割费标记的代数演算，通过添加部分确定性和可取消性的合理规则来处理Calcagno等人的分离代数的原始逻辑，同时保留割消除。我们通过一个合理的中间演算来证明我们演算的完备性，这个中间演算使我们能够从找不到证明的失败中构建反模型。然后，我们捕获其他命题抽象分离逻辑通过添加健全的规则不可分割的单位和不相交，同时保持完整性。我们提出了一个定理证明的基础上，我们的标记演算这些命题抽象分离逻辑。
2013-11-26 cs.LO
Subreflexive Logic: Completeness without Identity
Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院）
研究次自反逻辑，通过多种方式构建语义，包括引入海廷和布尔半代数、定义半伴随和单位等，证明其具有可靠且完备语义，能将蕴含解释为稳健后承，还允许句法消去切割，在经典情形下特定指称集语义也完备。
2026-07-28 cs.LO math.LO
Semantics for a Turing-complete Reversible Programming Language with Inductive Types
本文研究基于Theseus的高阶可逆编程语言，通过模式匹配保证函数可逆，证明其可编码任意可逆图灵机，构建了带模式匹配结构的并逆范畴语义，并证明其完全完备性，即可计算部分单射函数均为语言项的像。
2024-10-09 cs.LO
A Sound and Complete Hoare Logic for Dynamically-Typed, Object-Oriented Programs -- Extended Version --
定义了一种简单的动态类型、（纯粹的）面向对象语言。给出了一种结构化的操作语义和一种Hoare式的程序逻辑，用于在多个正确性概念中对语言中的程序进行推理。霍尔逻辑被证明是合理的和（相对）完整的，是-尽我们所知-第一个这样的逻辑动态类型的语言。
2016-01-08 cs.LO cs.PL
Optimal and Cut-free Tableaux for Propositional Dynamic Logic with Converse
本文给出了一个最优的（EXPTIME）、可靠的和完全的基于表的判定逆命题动态逻辑（CPDL）可满足性的算法，该算法不需要使用解析割。我们的主要贡献是一个健全的methodto结合我们以前的最佳方法跟踪最少不动点的PDL与我们以前的最佳方法处理逆的描述逻辑ALCI。扩展是不平凡的，因为这两个方法不能简单地组合。我们提供了足够的细节，以便其他人能够实现。我们的OCaml实现似乎是CPDL的第一个定理证明器。
2010-04-15 cs.LO
An Expressive Trace Logic for Recursive Programs
本文提出一种基于迹公式的可表达逻辑，为递归程序提供组合式指称语义和证明演算，并建立程序与公式间的 Galois 连接，揭示程序构造与逻辑连接词的对应关系。
2024-11-20 cs.LO cs.SE
First-Order Logic in Finite Domains: Where Semantic Evaluation Competes with SMT Solving
在本文中，我们比较了由数学模型检查器RISCAL支持的两种用于确定有限域上一阶公式有效性的替代机制：首先，语义评价的原始方法（基于RISCAL语言的指称语义的实现），第二，SMT求解的后一种方法（基于RISCAL公式到SMT-LIB公式的可满足性保持转换，作为SMT求解器的输入）。在简短介绍了这两种方法并讨论了它们的基本优点和缺点之后，我们通过一组人工基准和一组来自RISCAL实际应用的基准对它们进行了定量评估;为此，我们应用了最先进的SMT求解器Boolector，CVC 4，Yices和Z3。我们的基准测试表明，（虽然SMT解决一般大大优于语义评估），各种SMT求解器表现出很大的性能差异。更重要的是，我们确定类的公式，语义评估是能够竞争（甚至优于）可满足性解决，概述了一些改进的空间，在翻译的RISCAL公式SMT-LIB公式，以及在目前的SMT技术。
2021-09-07 cs.LO
Probabilistic modal μ-calculus with independent product
概率模态μ-演算是一种不动点逻辑，用于表示概率标记变迁系统（PLTS）的性质。两个等价的语义已经研究了这个逻辑，都分配给每个状态一个值在区间[0，1]表示的概率，该公式表示的属性在状态保持。一种语义是指称的，另一种是游戏语义，指定在两个玩家的随机奇偶游戏。概率模态μ演算的一个缺点是缺乏对PLTS的其他重要时态逻辑（如概率计算树逻辑（PCTL））进行编码所需的表达能力。为了解决这个问题，我们扩展了一对新的运营商的逻辑：独立产品和余产品。由此产生的逻辑，称为概率模态μ演算与独立的产品，可以编码许多感兴趣的属性，并纳入定性片段的PCTL。本文的主要贡献是为这种扩展的概率μ演算定义了一个合适的博弈语义。这依赖于一类新的游戏的定义，它通过允许一个游戏被分成并发的子游戏，每个子游戏独立地继续它们的进化，来概括标准的两个玩家随机（奇偶）游戏。我们的主要技术结果是两个语义的等价性。证明是在ZFC集合论中进行的，在不可数基数上扩展了Martin公理。
2012-11-26 cs.LO
HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories
我们提出了一个简单的决议证明系统高阶约束霍恩条款（HoCHC）-系统的高阶逻辑模理论-并证明其可靠性和反驳的完整性w.r.t.标准语义。作为推论，我们得到了HoCHC的紧性定理和半可判定性的背景理论，我们证明了HoCHC满足一个典型的模型性质。此外，从高阶到1阶逻辑的著名的翻译的一个变体被证明是健全的和完整的HoCHC在标准语义。我们说明了如何转移的可判定性结果（片段）一阶逻辑模理论，我们的高阶设置，作为例子的Bernays-Schonfinkel-Ramsey片段HoCHC模的限制形式的线性代数算术。
2019-04-19 cs.LO
A General Framework for Sound and Complete Floyd-Hoare Logics
本文将霍尔逻辑抽象为可追踪的对称monoidal范畴，这是系统理论的一个非常一般的框架。我们的抽象是基于一个跟踪monoidal函子从任意跟踪monoidal范畴到范畴的前序和单调关系。我们给出了几个例子，我们的理论如何概括通常的霍尔逻辑（部分正确的，而程序，部分正确的指针程序），并提供了一些案例研究，它可以用来开发新的霍尔逻辑（运行时分析，而程序和流电路）。
2008-07-07 cs.LO cs.OH
A sound and complete axiomatization for Dynamic Topological Logic
动态拓扑逻辑（DTL）是一种用于动力系统推理的多模态系统。它是语义定义的，因此，在该领域所做的大部分工作都是模型理论的。特别是，在所有动力系统的类上为DTL的完整语言找到一个完整的公理化的问题已被证明是相当难以捉摸的。在这里，我们建议丰富的语言，包括一个多元拓扑形态，最初介绍了Dawar和奥托在不同的上下文中。然后，我们提供了一个健全的公理化DTL在这个扩展的语言，并证明它是完整的。在我们的证明中，多元模态被以一种基本的方式使用。
2012-01-25 cs.LO math.LO
Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation
本文基于证明助手Isabelle/HOL，利用自由逻辑的浅层语义嵌入对范畴论进行元逻辑研究，形式化了初等拓扑斯与对称幺半闭范畴，并构建了易于使用的Isabelle范畴论库，为未来形式化研究奠定基础。
2023-06-16 cs.LO math.CT math.LO
An Asynchronous soundness theorem for concurrent separation logic
并发分离逻辑（CSL）是一种用于具有共享内存和锁的并发命令式程序的规范逻辑。在本文中，我们开发了一个并发和交互式帐户的异步游戏语义的启发逻辑。对于每个程序$C$，我们将一对异步转换系统$[C]_S$和$[C]_L$关联起来，它们描述了代码面对其环境或框架时的操作行为--在机器状态（$S$）和机器指令和锁（$L$）的级别上。然后，我们建立的每一个衍生树$π$的判断$Γ\vdash\{P\}C\{Q\}$定义了一个胜利和异步策略$[π]_{Sep}$相对于异步语义$[C]_S$和$[C]_L$。从这一点，我们推导出一个异步可靠性定理CSL，它指出，规范映射$\mathcal{L}:[C]_S\to[C]_L$从有状态语义$[C]_S$的无状态语义$[C]_L$满足一个基本的fibrational属性。我们主张，这提供了一个干净的和概念性的解释通常的CSL的可靠性定理，包括没有数据竞争。
2018-07-21 cs.LO cs.PL
From Matching Logic To Parallel Imperative Language Verification
程序验证是开发程序的证明系统，并证明证明系统相对于程序的可信操作语义的可靠性。然而，许多实用的程序验证器不是基于操作语义的，不能认真验证程序。提出了基于匹配逻辑的操作语义程序验证方法。本文在Grigore Ro{n}u的工作基础上，研究了并行命令式语言（PIMP）的匹配逻辑。根据我们的调查，本文是第一次研究的匹配逻辑的PIMP。在匹配逻辑中，我们将“无干扰”定义为字符并行规则，并证明了匹配逻辑对PIMP的操作语义的正确性。通过构造一个对配置模式执行符号化的逻辑语义重写的PIMP匹配逻辑验证器，将PIMP的操作语义和PIMP的验证形式化地联系起来，该验证器对PIMP的匹配逻辑是完善的。也就是说，我们的PIMP匹配逻辑验证器符合PIMP的操作语义。最后，通过一个并行程序设计中的标准问题，对匹配逻辑验证器进行了验证。
2021-02-08 cs.FL cs.LO
A sound interpretation of Leśniewski's epsilon in modal logic KTB
在本文中，我们将证明以下从Lehanniewski本体论的命题片段$\bf L_1$到模态逻辑$\bf KTB$的翻译$I^M$是合理的：对于$\bf L_1$的任何式$ϕ$和$ψ$，定义为\smallskip（M1）$I^M(ϕ\vee ψ)$ = $I^M(ϕ) \vee I^M(ψ),$（M2）$I^M(\neg ϕ)$ = $\neg I^M(ϕ),$（M3）$I^M(εab)$ = $\Diamond p_a \supset p_a . \wedge . \Box p_a \supset \Box p_b . \wedge . \Diamond p_b \supset p_a,$ \smallskip \noindent其中$p_a$和$p_b$是分别对应于名称变量$a$和$b$的命题变量。在最后一节中，我们将给出一些开放的问题和我的建议。
2021-10-02 cs.LO math.LO
Logic of Combinatory Logic
我们开发了一个经典的命题逻辑推理组合逻辑。我们定义了它的语法、公理系统和语义。以经典命题逻辑为基础，以类型化组合项为基本命题，给出了其语法和公理系统，并给出了其语义，该语义基于扩展了与原始组合子相对应的特殊元素的应用结构。无类型组合逻辑的方程理论和所提出的公理系统都被证明是正确和完整的。给出的语义。此外，我们证明了组合逻辑是可靠的和完备的w.r.t.给出的语义。
2022-12-13 cs.LO math.LO
A sound spatio-temporal Hoare logic for the verification of structured interactive programs with registers and voices
具有寄存器和语音的交互式系统（简称“rv系统”）是一种用于交互式计算的模型，该模型相对于时空对偶变换获得了闭寄存器机（“语音”是“寄存器”的时间对偶对应物）。同样的，AGAPIA v0.1，一种用于rv系统的结构化程序设计语言，是经典while程序（针对特定类型的数据）的时空对偶闭包。典型的AGAPIA程序描述了位于不同地点的开放过程，并具有对环境做出适当反应的时间窗口。该语言自然地支持流程迁移、结构化交互和在异构机器上部署组件。本文介绍了一种用于验证AGAPIA v0.1程序的类Hoare时空逻辑。作为一个案例研究，一个流行的分布式终止检测协议的形式化验证证明。
2008-10-19 cs.LO cs.PL
Cantor Derivative Logic in Topological Dynamics
基于康托导数算子的模态逻辑的拓扑语义产生了导数逻辑，也称为d-逻辑。与基于拓扑闭包算子的逻辑不同，d-逻辑以前没有在动态拓扑系统（DTS）的框架中研究过，动态拓扑系统是由配备有连续函数f的拓扑空间X组成的对（X，f）：X -> X。我们介绍了逻辑wK 4C，K4 C和GLC，并表明，他们都有有限Kripke模型的性质，是健全的和完整的d-语义在这个动态设置。我们还证明了一个一般性的结果的情况下，f是一个同胚，这产生的声音和相应的系统wK 4 H，K4 H和GLH的完整性。特别感兴趣的是GLC，它是基于分散空间的所有DTS的d-逻辑。我们利用GLC的完备性和离散空间的性质证明了原始三模态语言中的第一声和完备动态拓扑逻辑。特别是，我们表明，版本的DTL的基础上的类分散的空间是axiomatisable在原来的语言，自然axiomatisation是健全的和完整的。
2023-02-01 cs.LO math.LO
Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness
带测试的守护克莱因代数（GKAT）是KAT的一个有效片段，因为它允许等价的几乎线性可判定性。本文研究了GKAT的（余）代数性质。我们最初的重点是片段，可以区分不成功的程序执行不同的动作，通过省略所谓的提前终止公理。我们开发了一个操作（coalgebraic）和指称（代数）语义，并表明它们是一致的。然后，我们在这个语义的GKAT表达式的行为特征，导致一个coequation，捕捉对应于GKAT表达式的行为的自动机的共变。最后，我们证明了减少片段的公理是健全的和完整的w.r.t.的语义，然后建立在这个结果，以恢复一个语义，是健全的和完整的w.r.t.完整的公理集
2021-05-20 cs.LO cs.PL
Belief Semantics of Authorization Logic
授权逻辑已经在计算机安全理论中用于推理访问控制决策。在这项工作中，一个正式的信任语义授权逻辑。证明了信念语义是标准Kripke语义的继承。信念语义产生主体信念的直接表示，而不诉诸于Kripke语义中使用的技术机制。一个证明系统的逻辑，该系统被证明是健全的信念和Kripke语义。信念语义的可靠性证明，以及Kripke语义的变体，在Coq中是机械化的。
2013-08-04 cs.CR cs.LO
Doxastic Lukasiewicz Logic with Public Announcement
本文提出Łukasiewicz逻辑的信念扩展$BL^+$，进一步引入带公开宣告的逻辑$DL$，并用于建模模糊版泥孩子谜题，最后证明$DL$的可靠性与完备性。
2023-04-17 cs.LO math.LO
