Cofree coalgebras and differential linear logic
James Clift, Daniel Murfet
证明了向量空间中直觉线性逻辑的语义也是微分线性逻辑的一个模型，并且证明了上自由余代数的笛卡尔闭范畴是简单型微分λ演算的一个模型.
We prove that the semantics of intuitionistic linear logic in vector spaces which uses cofree coalgebras is also a model of differential linear logic, and that the Cartesian closed category of cofree coalgebras is a model of the simply-typed differential lambda calculus.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Sequoidal Categories and Transfinite Games: A Coalgebraic Approach to Stateful Objects in Game Semantics
引入博弈上的非交换序列算子$\oslash$，通过对博弈的张量积施加因果关系，从代数上捕捉博弈语义中历史敏感策略的状态存在.函子$A \oslash \_$的余代数--即从$S$到$A \oslash S$的态射--可以被看作是状态Transformers：如果$A \oslash \_$有一个最终的余代数$!A$，那么这样一个状态Transformer的变形封装了它的显式状态，这样它只在连续的调用之间共享。研究了$A \oslash \_$的最终余代数$!A$是$A$上的余自由交换余代数的载体的条件.也就是说，它是一个线性逻辑的指数模型，在这个模型中，我们可以在游戏语义设置中以共代数的方式构造命令对象，例如引用单元。证明了如果张量分解为序列，则最终余代数$!A$可被赋予余自由交换余代数的结构，如果存在从$!(A \times B)$到$!A \otimes !B$的自然同构.如果$!A$是$A \oslash \_$的双自由代数，这个条件总是满足的，但在一般情况下，有必要强加它，因为我们建立了一个例子，给出了一个sequoidally可分解的游戏类别，其中播放将被允许有超限长度。在这个范畴中，函子$A \oslash \_$的最终余代数不是A上的余自由交换余代数：我们通过明确地将函子$A \oslash \_$的最终序列与梅利斯、塔巴罗和塔森在构造余自由交换余代数时使用的作为极限…
Coalgebraic Semantics for Probabilistic Logic Programming
本文提出概率逻辑编程的余代数语义，通过函子F的余代数建模程序，并利用余自由余代数给出推导树与可能世界两种语义，可恢复分布语义，并扩展至加权逻辑编程。
Logic Column 15: Coalgebras and Their Logics
这篇文章介绍了最近的工作的主题指定的性质的过渡系统。通过给出一个适当的抽象描述的过渡系统作为余代数，它是可能的，以一种优雅的方式来获取这些过渡系统的性质的逻辑。
Predicate and relation liftings for coalgebras with side effects: an application in coalgebraic modal logic
我们研究了在存在副作用的情况下的共代数模态逻辑来验证行为等价性，即，当余代数存在于（余）Kleisli范畴或Eilenberg-Moore范畴中时。我们的目标是开发一个基于索引类别/纤维化的一般框架，这是常见的上述类别。特别是，我们展示了如何从关系提升（一种特殊的索引态射）的行为等价的coalgebraic概念，我们给出了一个一般的配方来构建这样的提升在上述三种情况下。最后，我们应用这个框架来获得（加权）语言等价和条件双相似性的逻辑特征。
Coalgebraic completeness-via-canonicity for distributive substructural logics
我们证明了强完备性的一系列的子结构逻辑相对于一个自然的偏序集为基础的关系语义使用一个coalgebrical版本的完整性，通过规范。通过形式化的问题，在语言的coalgebraic逻辑，我们开发了一个模块化的理论，涵盖了各种不同的逻辑在一个单一的框架下，并借给自己进一步扩展。此外，我们认为，共代数框架提供了一个系统的和原则性的方法来研究资源模型之间的关系，语义方面，和句法方面的子结构逻辑。
Systematic Construction of Temporal Logics for Dynamical Systems via Coalgebra
时态逻辑是动态系统的一种明显的高级描述性伴随形式主义，动态系统将行为建模为状态随时间的确定性演化。各种各样的不同的时间逻辑适用于动力系统存在，每个候选人都有自己的实用理由。在这里，提出了一种系统地构建动力系统时态逻辑的方法：首先，注意到动力系统可以以多种方式被视为余代数。其次，一个简单的标准结构的模态逻辑的余代数，即莫斯的余代数逻辑，应用。最后，所得到的系统的特点是相对于他们表达的时间属性。
Uniform Interpolation for Coalgebraic Fixpoint Logic
利用自动机与逻辑之间的联系，证明了一类广泛的余代数不动点逻辑具有一致插值性。为此，首先，我们推广的核心结果之一，在共代数自动机理论，即闭包下的投影，这是众所周知的，持有弱拉回保持函子，一类更一般的函子，即;具有准函子lax扩张的函子。然后证明了投影闭包蕴含互模拟量词的可定义性，最后证明了一致插值定理。
Category theoretic semantics for theorem proving in logic programming: embracing the laxness
命题逻辑程序$P$可以用程序中的原子命题集合上的$P_fP_f$ -余代数来标识。相应的$C(P_fP_f)$ -余代数，其中$C(P_fP_f)$是$P_fP_f$上的余自由余代数，描述了归结导子.使用宽松的语义，这种对应关系可以扩展到一类没有存在变量的一阶逻辑程序。由此产生的扩展捕获逻辑编程中的术语匹配分辨率的证明。完善宽松的方法，我们进一步扩展到任意逻辑程序。我们还展示了一个完善的Bonchi和Zanasi的饱和语义逻辑编程，补充宽松的语义。
A Categorical Approach to Coalgebraic Fixpoint Logic
本文提出一种基于序充实范畴的框架，将无交替不动点逻辑纳入余代数模态逻辑的对偶伴随体系，并证明最小解语义与初始代数语义等价，同时涵盖余代数$\mu$-演算、PDL及概率动态模态逻辑。
(Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras
行为等价可以通过互模拟、模态逻辑和破坏者-防御者博弈来表征。在本文中，我们回顾了这三个角度在一个coalgebraic设置，这使我们能够概括从特定的分支类型的过渡系统。我们感兴趣的定性概念（经典互模拟）以及定量概念（互模拟度量）。我们的第一个贡献是在经典的情况下，介绍了一个破坏者-防御者互模拟游戏的余代数。其次，我们介绍了这种游戏的度量的情况下，并进一步定义了一个实值模态共代数逻辑，从中我们可以得出的策略的扰流板。对于这个逻辑，我们展示了Hennessy-Milner定理的一个定量版本。
Duality for Fitting's Multi-valued Modal logic via bitopology and biVietoris coalgebra
本文通过扩展双拓扑对偶性并调整双Vietoris构造至成对布尔空间范畴，为Fitting多值模态逻辑建立了双拓扑与余代数对偶性，证明了其可靠性与完备性，并确立了Hennessy-Milner性质。
Non-iterative Modal Logics are Coalgebraic
模态逻辑是\emph{non-iterative}，如果它可以由不嵌套模态运算符的公理定义，并且\emph{rank-1}，如果公理中的所有命题变量都在模态运算符的范围内。众所周知，每一个语法定义的秩-1模态逻辑可以配备一个规范的共代数语义，确保可靠性和强完备性。在目前的工作中，我们将这一结果扩展到非迭代模态逻辑，表明每一个非迭代模态逻辑可以配备一个规范的coalgebraic语义定义的copointed函子，再次确保健全性和强完备性，通过一个规范的模型建设。在秩1的情况下，典型的余代数语义等价于具有适当框架条件的邻域语义，因此邻域语义上的非迭代模态逻辑的强完备性是已知的。作为这些结果的一个例子，我们讨论道义逻辑与事实分离，这是捕获的公理是非迭代的，但不是秩~1。
Coalgebraic trace semantics via forgetful logics
我们使用模态逻辑作为一个框架，共代数迹语义，并显示了具体的例子，如加权，交替和树自动机的语言语义的方法的灵活性，和生成概率系统的迹语义。我们提供了一个充分条件下，通过一个给定的确定性建设获得的逻辑语义符合跟踪语义。最后，我们考虑一个条件，保证存在一个规范的确定过程，是正确的，相对于一个给定的逻辑语义。这个过程与Brzozowski的最小化算法密切相关。
Monadic Second-Order Logic and Bisimulation Invariance for Coalgebras
推广标准的一元二阶逻辑的Kripke模型，我们介绍了一元二阶逻辑解释的余代数的任意集函子。一元二阶逻辑树相似的知名结果，我们提供了一个翻译的这种逻辑到一类自动机，相对于类的coalgebras承认一个树状支持Kripke框架。然后，我们考虑公式的行为等价下的不变性，更特别地，我们调查是否coalgebraic μ演算是一元二阶逻辑的bisimulation不变片段。最近的结果的第三作者的基础上，我们表明，为了提供这样一个共代数推广的Janin-Walukiewicz定理，它足以找到我们所谓的一个适当的一致建设的函子。作为这个结果的应用，我们得到了Janin-Walukiewicz定理的部分新证明，以及袋函子（分次模态逻辑）和所有指数多项式函子的互模拟不变性结果。最后，我们考虑了单调邻域函子的一些细节，它为单调模态逻辑提供了共代数语义。事实证明，这个函子没有足够的统一构造，因此互模拟不变性的自动机理论方法不能直接应用。如果我们考虑邻域模型之间的全局互模拟，这个问题可以克服：我们的主要技术结果之一提供了一个表征的单调模态μ演算扩展与全球模态，作为片段的一元二阶逻辑的单调邻域函子是不变的全局互模拟。
Generic Trace Logics
我们结合以前的工作，共代数逻辑与共代数轨迹语义的哈苏，雅各布斯和Sokolova。
Strong Completeness of Coalgebraic Modal Logics
规范模型在模态逻辑中具有核心重要性，特别是因为它们证明了强完备性和紧性。虽然规范模型的构造对于Kripke语义是很好理解的，但非正规模态逻辑通常存在微妙的困难-直到规范模型可能不存在的程度，例如在大多数概率逻辑中就是这种情况。在这里，我们提出了一个通用的规范模型建设的语义框架的共代数模态逻辑，它精确定位的语法和语义之间的一致性条件，保证强完备性的模态逻辑。我们应用这种方法来重建典型的模型定理，无论是已知的或民间传说，而且实例化我们的方法，以获得新的强完备性结果。特别是，我们证明了强完备性的分次模态逻辑与有限的多重性，模态逻辑的精确概率。
Linear-time logics -- a coalgebraic perspective
本文从余代数视角提出一种通用框架，通过结合分支行为与线性行为类型来定义线性时间逻辑，并证明其逐步语义与基于路径的语义等价，从而支持对定量系统中线性时间性质的可能性、似然性或最小代价进行推理。
Expressive Quantale-valued Logics for Coalgebras: an Adjunction-based Approach
该研究基于伴随框架，从刻画行为一致性的模态逻辑推导不动点方程，将其实例化到共代数场景，还得到线性时间下简洁的逻辑与不动点方程，并在分支、线性时间场景中验证了理论。
Continuation Semantics for Fixpoint Modal Logic and Computation Tree Logics
本文提出延续语义用于固定点模态逻辑和计算树逻辑，证明其与合取语义等价，并重新定义了 CTL* 的模型结构。
Logic programming: laxness and saturation
命题逻辑程序$P$可以用程序中的原子命题集合上的$P_fP_f$ -余代数来标识。相应的$C(P_fP_f)$ -余代数，其中$C(P_fP_f)$是$P_fP_f$上的余自由余代数，描述了归结导子.这种对应关系已经发展到两种方式，松散的语义和饱和的语义，局部有序的范畴和右Kan扩展的基础上，分别建模一阶程序。我们统一了这两种方法，展示它们作为互补而不是竞争，反映了逻辑编程的定理证明和证明搜索方面。在保持这种统一性的同时，我们进一步改进了松弛语义，给出了具有存在变量的逻辑程序的有限模型，并在逻辑程序中的变量和局部状态的世界之间建立了精确的语义关系。
Moss' logic for ordered coalgebras
本文为有序余代数提出一种有限性 Moss 余代数逻辑，采用单一覆盖模态和关系提升语义，证明了 Hennessy-Milner 性质并给出完备的相继式证明系统。
Coalgebraic Fuzzy geometric logic
本文旨在通过在模糊几何逻辑语言中加入模态来建立一个共代数模糊几何逻辑的框架。利用余代数的方法，用模糊几何逻辑的语言引入模态算子。为了定义模态算子，我们引入了模糊开谓词提升的概念。基于模糊拓扑空间和模糊连续映射范畴$\textbf{Fuzzy-Top}$上的闭函子$T$的余代数，建立了模糊几何逻辑的余代数模型。在这项工作中讨论了定义的模型的互模拟。
Proceedings of the First Workshop on Coalgebra, Horn Clause Logic Programming and Types
余代数，霍恩子句逻辑编程和类型研讨会于2016年11月28日至29日在爱丁堡举行。该研讨会标志着EPSRC授予的类型推断的共代数逻辑编程的结束。Komendantskaya，赫瑞瓦特大学和J. Power，巴斯大学，英国。
Using Coalgebras and the Giry Monad for Interpreting Game Logics --- A Tutorial
帕里克博弈逻辑的随机解释不应该遵循克里普克模型的通常模式，而克里普克模型又是基于吉里单子的克莱斯利态射，相反，需要一种特定的和更一般的概率非决定论方法。我们概述了这种方法连同其概率和测量理论的基础上，在悠闲的步伐介绍了吉里单子和Kleisli态射一起操纵它们的重要技术。证明建立具体的技术，并提供了现有的文献的指针。在完成本教程后，读者应该会发现在这个领域和相关领域更容易遵循原始文献，并且应该可以让她或他欣赏马尔可夫转移系统和随机有效性函数领域的原始工作的测量理论论点。
Graded Semantics and Graded Logics for Eilenberg-Moore Coalgebras
本文研究 Eilenberg-Moore 余代数的分级语义与分级逻辑，证明其能平滑实例化并产生表达性模态逻辑，同时通过量词值单子参数化框架涵盖等价与行为距离。
Coalgebraic Modal Logic for Dynamic Systems with Uncertainty
本文提出一类包含多种不确定性测度的多项式函子，用于构造表示不确定进程的余代数，并给出相应模态逻辑的公理、推理规则及基于典范余代数的完备性证明。
CoALP-Ty'16
本卷构成了研讨会上的预诉讼程序，霍恩子句逻辑编程和类型（CoALP-Ty'16），在爱丁堡举行的28- 29十一月2016作为EPSRC格兰特Coalgebraic逻辑编程类型推断结束的标志，由E。Komendantskaya和J. Power.本卷包括扩展摘要描述当前的研究在以下领域：语义：Lawvere理论和余代数在逻辑和函数式编程程序设计语言：霍恩子句逻辑类型推断在函数式语言和超越讨论后，在研讨会上的作者的扩展摘要将被邀请提交一份完整的文件，通过第二轮的裁判和选择的正式程序。
Fibred Coalgebraic Logic and Quantum Protocols
受应用于量子系统建模的启发，我们引入了一种新的余代数逻辑。我们的方法扩展了传统的谓词提升语义与额外的模态相关的条件不同的纤维。由于该构造的设置通常会涉及多个签名函子，因此该逻辑包含模态的演算，从而能够使用各种组合操作来构造新的模态。我们扩展的语义的共代数逻辑的设置，并证明这种扩展尊重行为等价。我们展示了如何在组合操作下保留模态的语义属性，然后应用我们的逻辑的计算方面来产生一组表达模态，用于推理量子系统，从更简单的组件构建这些模态。然后，我们展示了这些模态如何描述一些标准的量子协议。我们的逻辑的新功能，以允许统一的描述幺正演化，并支持本地推理，如“爱丽丝的量子位满足条件”是常见的讨论量子协议时。
Graded Monad Coalgebras for Continuous-Time Transition Systems
本文提出分级单调余代数用于建模连续时间转换系统，发展了分级余代数理论，并定义了分支时间和轨迹语义，同时开发了过程语义和状态不变性逻辑。
Categories and all that -- A Tutorial
这是对范畴的一个简短的介绍，重点是余代数。我们从介绍基本概念（范畴，函子，自然变换）开始，转向Kleisli tripel和monad，并简短讨论Haskell中的monad，然后继续展示代数，代数和monad之间的相互作用。讨论了余代数在模态逻辑语义中的应用，并对余代数逻辑作了简要介绍。发展是通过例子来说明，通常采取从应用到计算机科学，具有一定的偏好随机系统。
A Coalgebraic Semantics for Intuitionistic Modal Logic
本文利用 Esakia 空间到 Priestley 空间包含的右伴随，为带 $\Box$ 的直觉主义模态逻辑建立余代数语义，并应用于互模拟、自由模态 Heyting 代数对偶及余代数直觉主义逻辑理论。
Strongly Complete Logics for Coalgebras
函子的余代数以统一的方式模拟不同类型的转移系统。本文主要讨论了集基余代数有限逻辑的统一描述。特别地，给出了从任意集合函子构造逻辑的一般方法，并在附加的假设下证明了该方法是强完备的。我们分三部分进行。第一部分论证了筛余极限保持函子是指保持泛代数结构的函子。我们的主要定理在这里指出，函子保持筛选余极限当且仅当它有一个有限的表示的操作和方程。此外，函子的代数范畴的表示是从基础范畴和函子的表示中合成地获得的。第二部分研究了在ind-completions上函子的代数，并将Jo nsson和Tarski关于带算子的布尔代数的典型扩张的定理推广到了这个情形。第三部分在第一部分的基础上展示了如何将有限逻辑与任何有限集保持函子T相关联。在第二部分的基础上，我们证明了在T上的一个合理条件下，该逻辑是强完备的。
Expressive Logics for Coinductive Predicates
本文在余代数一般框架下研究逻辑对余归纳谓词的完全表征，提出充分性与表现性条件，并应用于相似性、发散性及自动机行为度量等实例。
Logic-Induced Bisimulations
对于由逻辑连接给出的共代数模态逻辑，我们定义了一个新的逻辑诱导的互模拟概念（称为$ρ$ -互模拟），并研究了它的性质。我们表明，它是结构的意义上说，它是只在定义方面的余代数结构和一步模态语义，而且，可以通过一种形式的关系提升的特点。此外，我们比较$ρ$ -互模拟几个著名的等价概念，我们证明了两个模型之间的互模拟的集合往往形成一个完整的晶格。主要的技术结果是一个Hennessy-Milner型定理，它指出，在某些条件下，逻辑等价意味着$ρ$ -双相似性。特别地，后者不依赖于函子\emph{not}（余代数的类型）和$\mathsf{L}$（给出逻辑）之间的对偶性，也不依赖于逻辑连接$ρ$的属性。
Lifting Coalgebra Modalities and $\mathsf{MELL}$ Model Structure to Eilenberg-Moore Categories
本文在Eilenberg-Moore范畴中为线性逻辑的MELL片段建立模型，通过定义带混合分配律的Hopf单子作为MELL提升单子，证明线性范畴结构可提升至其代数范畴，并利用余代数范畴中的群构造此类单子。
Quantum Field Theory and Coalgebraic Logic in Theoretical Computer Science
在本文中，我们建议，在范畴论的框架下，它是可能的，以证明数学和逻辑之间的\textit{dual equivalence}的$q$ -变形的Hopf余代数的范畴和QFT的$q$ -变形的Hopf代数的范畴，解释为热场论。每一对代数-余代数分别刻画了QFT系统和它的镜像热浴，从而在远离平衡的条件下持续地模拟耗散量子系统，这对生物科学也具有明显的意义。$q$ -变形的Hopf余代数和$q$ -变形的Hopf代数构成了两个对偶范畴，因为它们分别由与Bogoliubov变换有关的同一函子$T$和它的逆变应用$T^{op}$刻画.实际上，\textit{q} -变形参数与Bogoliubov角有关，并且它是有效的热参数。因此，$q$的不同值可以明确地识别并标记出量子真空的叶理过程中出现的真空。这意味着，在泛余代数的框架下，作为动力学和计算系统（“标记状态转移系统”）的一般理论，这样标记的无限多个量子真空可以被解释为“无限状态黑箱机”的最终余代数。所有这些都为基于QFT的这种共代数公式设计一类新的通用量子计算架构开辟了道路，因为它自然生成斐波那契级数的能力证明了这一点。
Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings
线性逻辑的许多模型是基于或密切相关的线性代数，在这个意义上，态射是“矩阵”在适当的系数集。例子包括基于相干空间、有限性空间和概率相干空间的模型，以及关系和加权关系模型。本文引入了一个基于模块理论的统一框架，使上述模型的线性代数方面更加明确。具体来说，我们考虑模块上的西格玛半环$R$，这是环状结构的部分定义可数和，并表明，在上述模型中的态射实际上是$R$ -线性映射在标准的代数意义上适当的$R$。我们的代数处理的一个优点是，$R$ -模范畴是局部可表示的，从这一点很容易得出，这一范畴成为一个模型的直觉线性逻辑与cofree指数。然后，我们讨论了经典模型的构造，并表明上述模型是我们构造的例子。
Logic and linear algebra: an introduction
我们给出了一个专门为代数学家逻辑的介绍，解释如何证明线性逻辑可以被视为算法，用于构造态射在对称封闭的幺半范畴与额外的结构。通过展示如何将线性逻辑中的证明表示为向量空间之间的线性映射，这一点变得明确。这个向量空间语义有趣的部分是基于Sweedler的余自由余交换余代数。
Steps and Traces
在余代数理论中，迹语义可以用各种不同的方式定义，包括通过代数逻辑，单子的Kleisli范畴或它的Eilenberg-Moore范畴。本文阐述了两个新的统一思想：1）余代数迹语义自然地提出了在余递归代数，2）所有三种方法出现作为相同的抽象设置的实例。我们的观点将不同的方法置于一个共同的屋檐下，并允许推导出其中一些方法重合的条件。
Bialgebraic Semantics for Logic Programming
双代数提供了一个抽象框架，包含不同类型的计算模型的语义。在本文中，我们提出了一个双代数方法的语义逻辑程序设计。我们的方法是研究逻辑程序作为反应系统，并利用抽象技术开发的设置。首先，我们使用饱和度模型的操作语义的逻辑程序作为余代数上的预层。然后，利用预层上的双代数，明确了其代数结构。由此产生的语义原来是组合方面的连接和长期替代。此外，它还编码了一个并行计算模型，其可靠性由不同线程之间的内置同步概念保证。
COOL 2 -- A Generic Reasoner for Modal Fixpoint Logics
本研究开发了面向代数模态不动点逻辑的通用推理器COOL 2，可实例化为多种模态逻辑的推理工具，并在多类基准集上完成了评估。
Coalgebras, Chu Spaces, and Representations of Physical Systems
我们回顾了我们以前的工作表示量子系统作为朱空间，并研究使用余代数作为一个替代框架。一方面，余代数允许重复测量的动态被捕获，并提供数学工具，如最终余代数，互模拟和余代数逻辑。然而，标准的共代数框架不适应逆变，并且过于严格，不允许物理对称性被表示。我们在余代数上引入了一种纤维化结构，其中的逆变由索引表示。我们使用这种结构给出了一个通用的语义量子系统的基础上最终的余代数建设。我们的特点平等在这个语义作为投射等价。我们还定义了一个类似的索引结构的Chu空间，并使用此获得一个新的范畴描述的Chu空间的范畴。利用Chu空间和共基上余代数的指标结构，定义了从余代数到Chu空间的截断函子。这个截断函子是用来提升到朱空间的希尔伯特空间的物理对称的广群的完整和忠实的表示，在我们以前的工作中获得的，共代数语义。
Relating Structure and Power: Comonadic Semantics for Computational Resources
组合对策在有限模型理论、约束满足、模态逻辑和并发理论中被广泛用于刻画结构之间的逻辑等价性。特别是，Escherichfeucht-Fraisse游戏，卵石游戏和互模拟游戏发挥了核心作用。我们展示了如何这些类型的游戏可以描述在一个索引的家庭comonads的关系结构和同态的类别。索引k是限制对底层结构的访问程度的资源参数。这些comonads的coKleisli范畴可以用来给出广泛的重要逻辑等价的无语法刻画。此外，这些索引comonad的共代数可以用来表征关键的组合参数：树深度的Escherichfeucht-Fraisse comonad，树宽度的卵石comonad，和同步树深度的模态展开comonad。这些结果铺平了道路，系统的两个主要分支之间的联系领域的逻辑在计算机科学迄今已几乎脱节：范畴语义学，有限和算法模型理论。
Quantitative Graded Semantics and Spectra of Behavioural Metrics
本文提出定量分级语义框架，统一处理行为度量谱，并给出实值模态逻辑刻画行为距离的一般准则，应用于模糊度量转移系统获得新的迹距离特征逻辑。
Graded Monads and Graded Logics for the Linear Time -- Branching Time Spectrum
并发系统的基于状态的模型传统上被认为是在各种概念下的进程等价。在标记的过渡系统的特定情况下，这些等价的范围从跟踪等价（强）的双相似性，并组织在什么是所谓的线性时间分支时间谱。通用的共代数和分级单子的组合提供了一个通用的框架，在该框架中，并发的语义可以参数化的分支类型的底层过渡系统和粒度的进程等价。我们表明，在本文件中，这一框架的分级语义subanimate最重要的等价物从线性时间分支时间谱。分级语义的一个重要特征是它允许特征模态逻辑的原则性提取。我们已经建立了这些分级逻辑的不变性下，在早期的工作中给定的分级语义，在本文中，我们扩展了逻辑框架与一个明确的命题层，并提供了一个通用的表达标准，概括了经典的亨尼西-米尔纳定理粗糙的概念过程等价。我们提取分级逻辑的一系列分级语义标记的过渡系统和概率系统，并给出示例性的证明，他们的表现力的基础上，我们的通用标准。
Fixpoint constructions in focused orthogonality models of linear logic
本文研究线性逻辑聚焦正交性范畴中的不动点构造理论，通过证明初始代数和终余代数的提升定理，为带类型最小和最大不动点的模型提供公理化范畴框架，并扩展至域论中双自由代数的提升。
Graded Differential Categories and Graded Differential Linear Logic
本文提出了分级微分线性逻辑（GDiLL）的矢列演算及其范畴语义（分级微分范畴），利用余关系和推导变换构建理论框架，证明对称幂可生成此类范畴，并探讨多种模态的分级版本及其实际应用。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。