微分动态逻辑的一致替换演算

一种简化的悬置演算及其与其它显式代换演算的关系

A Simplified Suspension Calculus and its Relationship to Other Explicit Substitution Calculi

本文讨论了λ演算中代换的显式处理。它的贡献之一是简化和合理化的暂停演算，体现了这样的待遇。这个演算的早期版本提供了一个繁琐的替换组合编码，这是一个对有效实现约简很重要的操作。这里简化了这种编码，从而产生了易于在应用程序中直接使用的处理。合理化包括消除在解开替换时实际上无关紧要的灵活性，这种灵活性具有丢失术语中上下文信息的无意副作用;修改后的演算现在具有自然支持逻辑分析的结构，例如与类型分配有关的结构，在lambda术语上。整体演算具有令人满意的理论性质，如强终止子演算的替代和汇合，即使在存在长期Meta变量，符合嫁接解释。本文的另一个贡献是确定了一系列广泛的属性，这些属性是显式替换演算所需的，并基于这些属性对各种拟议系统进行分类。悬浮演算是作为一种工具，在这项研究中。特别是，映射之间的描述，它和其他结石对理解后者的特点。

微分对策逻辑的一致替换

Uniform Substitution for Differential Game Logic

本文提出了一种微分对策逻辑的一致替换演算（dGL）.丘奇的统一替换在任何地方都用一个项或公式代替一个函数或谓词符号。在将它们推广到微分博弈逻辑并允许用混合博弈替换博弈符号之后，统一替换使得只使用公理而不是公理模式成为可能，从而大大简化了实现。而不是微妙的模式变量和健全的关键侧条件的逻辑变量的出现模式，以限制无限多的公理模式实例健全的，由此产生的公理化只采用了有限数量的普通dGL公式作为公理，统一的替代实例健全。本文证明了单调模态逻辑dGL的一致替换的可靠性和完备性。由此产生的公理化承认一个简单的模块化实现dGL定理证明。

lambda演算中的替换与Curry学派的作用

Substitution in the lambda Calculus and the role of the Curry School

本文探讨了lambda演算中替换与alpha同余的相互依赖问题，指出Curry学派的研究优雅地解决了这一让学生困惑的难题，以此颂扬其在替换与alpha同余领域的贡献。

语境类型论的显式替代

Explicit Substitutions for Contextual Type Theory

在本文中，我们提出了一个显式的替代演算，区分普通的约束变量和元变量。它的类型原则是从语境模态类型论中衍生出来的。首先，我们提出了一个依赖类型的λ演算与普通变量的显式替换和元变量的显式元替换。然后，我们提出了一个弱头规范化过程，执行两个替代懒惰，并在一个单一的通行证，从而结合替代走两个不同类别的变量。最后，我们描述了一个双向的类型检查算法，使用弱头规范化和证明的可靠性。

证明网与线性代换演算

Proof Nets and the Linear Substitution Calculus

从线性逻辑理论的一开始，就知道如何将$λ$ -演算表示为线性逻辑证明网。然而，这两个系统具有不同的粒度，特别是证明网具有显式的共享概念-指数-和微步操作语义，而$λ$演算没有共享和小步操作语义。在这里，我们表明，\emph{linear substitution calculus}，一个简单的改进的$λ$ -演算与共享，是同构的证明网在操作层面。尽管如此，两个不同的共享项仍然可以具有相同的证明网表示-进一步的结果是证明网在共享项上诱导的相等性的特征。最后，这样的条款和证明网之间的关系的详细分析，提出了一个新的，抽象的概念证明网，重写的考虑，不一定是图形的性质。

λ演算标准化定理的构造类型论形式化

Formalization in Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using Multiple Substitution

我们提出了一个完整的形式化的标准化定理的Martin-Löf的构造类型论的λ演算使用一阶语法与一种名称的自由和绑定变量和斯托顿的多重替代。我们的形式化是基于Ryo Kashima的证明，其中具有标准序列的beta-约简的概念被归纳关系捕获。证明只使用结构归纳法的语法和定义的关系，这是可能的，由于我们采用的特定公式的替代。整个开发过程使用Agda系统进行了机器检查。

显式代换组合学

Combinatorics of explicit substitutions

$λ\upsilon$是$λ$ -演算的扩展，它内化了替换演算。在当前的文件中，我们调查的组合性质的$λ\upsilon$专注于定量方面的替代决议。我们表现出一个意想不到的计数序列之间的对应关系$λ\upsilon$ -条款和著名的加泰罗尼亚数字。作为一个副产品，我们建立了有效的随机$λ\upsilon$ -条款的抽样计划。我们表明，典型的$λ\upsilon$ -条款表示，在很强的意义上，在经典的$λ$ -演算的非严格计算。此外，典型地，几乎所有的替换实际上都在闭包下被暂停，即未被评估。因此，我们认为，$λ\upsilon$是一个内在的非严格演算的显式替换。最后，我们研究了$λ\upsilon$中控制替代分辨率的各种赎回权的分布，并研究了各种替代原语的定量贡献。

基于显式替换的线性λ演算在深度推理中的证明搜索

Linear lambda Calculus with Explicit Substitutions as Proof-Search in Deep Inference

SBV是一个深度推理系统，它用非交换算子Seq扩展了乘法线性逻辑的逻辑算子集。本文引入了一个逻辑系统SBVr，它通过在SBV上增加一个自对偶原子重命名算子而扩展了SBV，并证明了在SBVr上割消元成立。SBVr和它的无割子系统BVr是关于带显式替换的线性λ演算的完备和可靠的.在任何策略下，一旦M被映射成SBVr的公式，则任何线性矩阵项M的求值步骤序列就变成SBVr（BVr）中的证明搜索过程。完整性和可靠性来自于用显式替换作为过程来模拟线性beta约简。SBVr的新重命名操作符的作用是按需重命名通道名称。这模拟了在β还原中发生的取代。尽管SBVr是SBV的最小扩展，但它的证明搜索可以计算所有的布尔函数，因为带有显式替换的线性代数演算也可以计算所有的布尔函数。因此，SBVr和BVr的证明搜索至少是ptime-complete的。

资源控制lambda演算和使用交集类型的显式替换之旅（一个帐户）

A journey through resource control lambda calculi and explicit substitution using intersection types (an account)

在本文中，我们邀请读者通过三个lambda演算与资源控制的旅程：lambda演算，lambda演算和lambda演算与显式替换。由于弱化和收缩运算符的存在，这三种演算都可以显式控制资源。在这个过程中，我们提出了所有三个资源控制演算的交集型分配系统。我们认识到需要三种变量都需要不同类型的交叉点类型。我们的主要贡献是在所有三个结石的减少强规范化的特点，使用的技术reductionary，头部主题扩展，以及订单和适当的嵌入的条款相结合。

走向$λ$ -演算中替换解析的平均案例分析

Towards the average-case analysis of substitution resolution in $λ$-calculus

替换解析支持$β$ -归约的计算特性，通过避免捕获的绑定变量项交换来补充其执行。唉，替换的元级定义，掩盖了一个非平凡的计算，把$β$ -归约变成了一个原子重写规则，尽管它的操作复杂度不同。在本文中，我们提出了一个有点间接的平均情况下分析的替代决议在经典的$λ$演算，在$λ\upsilon$，一个扩展的$λ$演算内化的显式替代的$\upsilon$演算的替代定量分析的基础上。在这个框架内，我们表明，对于任何固定的$n \geq 0$，一个均匀随机的概率，条件的大小，$λ\upsilon$ -长期$\upsilon$ -规范化在$n$正常顺序（即最左最外）减少步骤往往是一个可计算的限制，长期大小趋于无穷大。为此，我们建立了一个有效的层次结构$\left(\mathscr{G}_n\right)_n$的定期树文法分区$\upsilon$ -规范化条款到类的条款规范化在$n$正常顺序重写步骤。在我们的建设的主要技术成分是一个归纳的方法来建设$\mathscr{G}_{n+1}$出$\mathscr{G}_n$的基础上，反过来，有限的交集分区的算法建设，罗宾逊的统一算法的启发。最后，我们简要地讨论了我们的方法的应用程序，其他长期重写系统，集中在两个密切相关的形式主义，即完整的$λ\upsilon$演算和组合逻辑。

使用交集类型线性化显式替换

Linearising Explicit Substitutions using Intersection Types

研究为带显式替换的演算定义新项展开，以此关联带显式替换的lambda演算与Boudol的带多重性的资源感知lambda演算，函数参数可用性或受限，核心方法是新项展开，主要贡献是建立了这种关联。

按值调用λ演算机的形式化小步验证

Formal Small-step Verification of a Call-by-value Lambda Calculus Machine

我们正式验证一个抽象的机器调用的值的alcuda演算与de Bruijn条款，简单的替代，和小步语义。我们遵循逐步改进的方法，从一个带有替换的朴素堆栈机器开始。然后，我们细化到一个具有闭包的机器，最后是一个具有为闭包提供结构共享的堆的机器。我们证明了三个细化步骤的正确性与组成小步自下而上的模拟。有一个附带的Coq开发验证所有结果。

指数作为替换与线性逻辑中切割消除的代价

Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic

本文提出指数替换演算（ESC），基于显式替换思想为IMELL切割消除提供新表示，设计了具有子项性质的切割消除策略，首次为无约束指数的切割消除提供多项式代价模型，并证明了无类型合流与有类型强规范化。

基于树序列演算的友谊认知逻辑公理化

Axiomatizing Epistemic Logic of Friendship via Tree Sequent Calculus

本文积极地解决了Seligman、Girard和Liu等人提出的友谊认知逻辑是否能提供一个希尔伯特系统的问题。为了找到一个Hilbert系统，我们首先介绍了一个健全的，完整的和无割的树（或嵌套）EFL演算，这是一个集成的组合Seligman的基本混合逻辑的树演算和模态逻辑的树演算。然后，我们将树的结构转换成一个普通的公式来指定EFL的Hilbert系统，最后证明我们的Hilbert系统对于预定的二维语义是健全和完备的。

λ演算和一阶逻辑中的克隆和Genoid

Clones and Genoids in Lambda Calculus and First Order Logic

基因型是两个对象的范畴，其中一个是自身与另一个的产物。一个genoid可以看作是一个抽象的置换代数。这是一个值得注意的事实，这样一个简单的概念，可以用来提供一个统一的代数方法，λ演算和一阶逻辑。

A cut-free sequent calculus for the bi-intuitionistic logic 2Int

The purpose of this paper is to introduce a bi-intuitionistic sequent calculus and to give proofs of admissibility for its structural rules. The calculus I will present, called SC2Int, is a sequent calculus for the bi-intuitionistic logic 2Int. Calculi for this logic represent a kind of bilateralist reasoning, since they do not only internalize processes of verification or provability but also the dual processes in terms of falsification or what is called dual provability. A normal form theorem for a natural deduction calculus of 2Int has already been stated, in this paper I want to prove a cu…

逻辑程序设计中的答案替换问题

On Answer Substitutions in Logic Programming

答案替换在逻辑编程中起着核心作用。为了支持{ \it selective}答案替换，我们将目标中的$\exists x$细化为两个不同的版本：噪声版本$\exists^o x$和无声版本$\exists x$。主要区别在于，只有$\exists^o x$中的实例化才会记录在答案替换中。$\forall x$也是如此。此外，我们还讨论了无关常数和未知常数的概念。

用组合逻辑理解元程序设计中不卫生替换的表达能力

Understanding the Expressive Power of Unhygienic Substitution in Metaprogramming via Combinatory Logic

最近的工作组合逻辑演示了一个组合翻译从λ演算，使意义开放的条款。由于开放术语的含义是元编程研究中的一个关键难点，我们研究这种想法是否可以扩展到元编程系统与卫生和不卫生的替代，特别是$λ_{e}^{\rightarrow \Box}$和$λ_{\mathcal{S}}$。我们的结论是，有定量的证据来支持索赔，元编程与不卫生的替代是更强大的元编程与卫生的替代。

First-Order Game Logic and Modal Mu-Calculus

This paper investigates first-order game logic and first-order modal mu-calculus, which extend their propositional modal logic counterparts with first-order modalities of interpreted effects such as variable assignments. Unlike in the propositional case, both logics are shown to have the same expressive power and their proof calculi to have the same deductive power. Both calculi are also mutually relatively complete. In the presence of differential equations, corollaries obtain usable and complete translations between differential game logic, a logic for the deductive verification of hybrid ga…

交换：命名和索引显式替换演算之间的自然桥梁

Swapping: a natural bridge between named and indexed explicit substitution calculi

这篇文章致力于介绍lambda_rex，一个显式的替代演算与de Bruijn指数和一个简单的符号。通过与lambda_ex（一种最近的变量名称形式）同构，lambda_rex实现了beta-约简（Sim）的模拟，beta-强归一化（PSN）和元融合（MC）的保留，以及其他理想的属性。我们的演算基于lambda_dB的一种新的表示，使用了最初由de Bruijn设计的交换概念。除了lambda_rex，另外两个索引演算同构的lambda_x和lambda_xgc，展示了我们的技术应用于设计的索引版本的已知命名演算的潜力。

微积分风格的交集逻辑

Intersection Logic in sequent calculus style

交型赋值系统直接设计为将直觉逻辑的蕴涵和合取片断的公式赋值给代数演算的项的演绎系统。但它与逻辑的关系并不规范。所有的逻辑之间，已被提出作为其基础，我们认为ISL，它给出了一个逻辑解释的交集分裂的直觉合取成两个连接词，分别与本地和全球的行为，是当地的交集。我们认为ISL是一个有趣的逻辑本身，为了支持这一说法，我们给它的微积分制定，我们证明了它享有削减消除属性。

可计算性逻辑中递归性的顺演算驯服，第I部分

The taming of recurrences in computability logic through cirquent calculus, Part I

本文构造了一个相应的演算系统，并从可计算性逻辑的语义角度证明了它的可靠性和完备性（见http：//www.cis.upenn.edu/paggiorgi/cl.html）.该系统的逻辑词汇包括否定、平行合取、平行析取、分支递归和分支共递归。这篇文章分两部分发表，（现在的）第一部分包含了一个完整性证明和一个可靠性证明，（即将出版的）第二部分包含了一个完整性证明。

可计算性逻辑中递归性的顺演算驯服，第II部分

The taming of recurrences in computability logic through cirquent calculus, Part II

本文构造了一个相应的演算系统，并从可计算性逻辑的语义角度证明了它的可靠性和完备性（见http：//www.cis.upenn.edu/paggiorgi/cl.html）.该系统的逻辑词汇包括否定、平行合取、平行析取、分支递归和分支共递归。这篇文章分两部分发表，（前）第一部分包含了一个完整性证明，（现在）第二部分包含了一个完整性证明。

动态拓扑逻辑的一个序列演算

A Sequent Calculus for Dynamic Topological Logic

本文对动态拓扑逻辑$\textbf{DTL}$的时间-拓扑片段$\textbf{DTL}_{0}^{\circ * \slash \Box}$引入了一个新的演算，利用\cite{paper3}中给出的$\textbf{DTL}_{0}^{\circ * \slash \Box}$的公理化，从语义上证明了其可靠性，并从语法上证明了其完备性. $\textbf{DTL}_{0}^{\circ * \slash \Box}$的无割的Tumbler演算是Gentzen经典Tumbler演算的命题片段、模态扩展的两个$\Box$结构规则、以及时间扩展的九个$\circ$（下一个）和$*$（下一个）结构规则的结合。未来的研究将集中在动态拓扑$\textbf{S5}$逻辑的超代数演算的建设，以证明Kremer的下一个删除猜想几乎离散空间$\textbf{S5H}$上的同胚逻辑。

命令注入攻击、延续和Lambek演算

Command injection attacks, continuations, and the Lambek calculus

本文展示了命令注入攻击，延续和Lambek演算之间的联系：某些命令注入，如对SQL的重言式攻击，被证明是一种控制效果的形式，可以使用Lambek演算进行类型化，推广了延续的双重否定类型。Lambek的句法演算是一个逻辑，其中两个隐含连接词分别从左和右获取它们的论点。这些连接词描述了在构建句法结构时，字符串如何与它们的左右上下文相互作用。微积分是一种没有结构规则的命题逻辑，因此是线性逻辑和分离逻辑等子结构逻辑的先驱。

可计算性逻辑的命题圆环演算

A propositional cirquent calculus for computability logic

本文提出CL18公理化系统，用于可计算性逻辑的基本命题片段，并证明其相对于该逻辑博弈语义的可靠性与完备性。

一种用于双模可证性逻辑的非良基带标记序列演算

A Non-Wellfounded and Labelled Sequent Calculus for Bimodal Provability Logic

本研究针对双模可证性逻辑CS，基于类Kripke语义建模构建带标记非良基演算系统，借助循环证明理论实现逆良基性，证明系统的可靠性与完备性，同时给出原始判定程序和反模型提取方法。

无需复制粘贴的替换

Substitution Without Copy and Paste

针对带绑定语言定义替换需重复定义替换与重命名的问题，提出一种避免重复的轻量级方法，生成同构于初始简单类型CwF的范畴，并以文学化Agda脚本呈现。

λ演算的证明逻辑

Justification Logic of the Lambda Calculus

研究λ演算的证明逻辑，通过引入一种逻辑，其模态证明项为类型化λ项，能同时推理计算与证明。给出公理系统、自然演绎系统及Curry-Howard解释，还构建相继式演算并证明切割消去，得到归一化结果。

Coq 中替换引理的形式化扩展

A Formalized Extension of the Substitution Lemma in Coq

本文在 Coq 中形式化验证了扩展显式替换算子后的 lambda 演算语法下替换引理仍然成立，采用 nominal 方法处理 alpha 等价，为不同显式替换演算提供了通用框架。

Display to Labeled Proofs and Back Again for Tense Logics

We introduce translations between display calculus proofs and labeled calculus proofs in the context of tense logics. First, we show that every derivation in the display calculus for the minimal tense logic Kt extended with general path axioms can be effectively transformed into a derivation in the corresponding labeled calculus. Concerning the converse translation, we show that for Kt extended with path axioms, every derivation in the corresponding labeled calculus can be put into a special form that is translatable to a derivation in the associated display calculus. A key insight in this con…

公式大小游戏与模态替换演算的模型检验

Formula size game and model checking for modal substitution calculus

本文通过公式大小游戏研究了MSC及其扩展的表达能力和模型检验复杂度，证明其与图灵机、mu演算等的复杂度关系，并建立了相关逻辑的复杂度分类。

证明逻辑的加标序列演算与反模型构造

Labeled Sequent Calculus and Countermodel Construction for Justification Logics

本文针对证明逻辑及混合模态-证明逻辑提出加标序列演算，内化Fitting模型语义，证明其弱子公式性质、规则可逆性等性质，建立可靠性完备性，给出可终止的证明搜索与反模型构造流程及模型对应关系。

通过亚原子逻辑和受保护替换的证明压缩

Proof Compression via Subatomic Logic and Guarded Substitutions

本文提出受保护替换机制，用于亚原子逻辑中的证明压缩，通过仅替换自由变量的受保护出现来构造推导叠加，实现无需切割规则即可p-模拟带替换的Frege系统。

一种面向替换的模态方法

A modal approach towards substitutions

本文针对复杂场景下迭代替换的建模需求，提出了可同时刻画单步与迭代替换的模态逻辑框架，分析了其表达能力等性质，明确了与经典逻辑句法替换及现有迭代推理框架的关联与优势。

可计算性逻辑的流演算系统CL6的可靠性和完备性

Soundness and completeness of the cirquent calculus system CL6 for computability logic

可计算性逻辑是可计算性的形式化理论。Japaridze的早期文章“Introduction to Cirquent Calculus and Abstract Resource Semantics”证明了可计算性逻辑的基本片段CL5的可靠性和完备性。本文将这一结果扩展到更具表现力的cirquent演算系统CL6，这是CL5和经典命题逻辑的保守扩展。

映射融合与同步超边替换到逻辑程序设计中

Mapping Fusion and Synchronized Hyperedge Replacement into Logic Programming

在本文中，我们比较了三种不同的形式主义，可用于该地区的模型，分布式，并发和移动系统。特别是，我们分析了进程演算，融合演算，图形变换中的同步超边替换与霍尔同步（HSHR）的方法和逻辑编程之间的关系。我们提出了一个翻译融合演算到HSHR（而融合演算使用米尔纳同步），并证明了融合演算和HSHR转换的减少语义之间的对应关系。我们还提出了一个映射从HSHR到一个事务版本的逻辑编程，并证明有一个完整的对应关系之间的两个形式主义。从融合演算到逻辑编程的映射是有趣的，因为它显示了两种形式主义之间的紧密类比，特别是在处理名称生成和移动性方面。根据HSHR的中间步骤是方便的，因为图转换允许多个远程同步，如Fusion Calculus语义所要求的。

A Labelled Sequent Calculus for Public Announcement Logic

Public announcement logic(PAL) is an extension of epistemic logic (EL) with some reduction axioms. In this paper, we propose a cut-free labelled sequent calculus for PAL, which is an extension of that for EL with sequent rules adapted from the reduction axioms. This calculus admits cut and allows terminating proof search.

直觉主义强Löb逻辑的新演算：强终止性与消割，形式化

A new calculus for intuitionistic Strong Löb logic: strong termination and cut-elimination, formalised

本文为直觉主义强Löb逻辑提出新相继式演算，实现强终止的向后搜索与句法消割，并在Coq中形式化验证。

初等基圆积分I：平行和选择连接词

Elementary-base cirquent calculus I: Parallel and choice connectives

循环演算是一个证明系统，操纵循环风格的结构，而不是公式。利用它，本文构建了可计算性逻辑命题片段（计算问题的博弈语义构想逻辑，见http://www.csc.villanova.edu/~japaridz/CL/）的一个合理而完整的公理化CL 16，其逻辑词汇由否定、平行和选择连接词组成，其原子表示基本的，即无移动的博弈。

余代数μ演算的EXPTIME表

EXPTIME Tableaux for the Coalgebraic mu-Calculus

模态逻辑的共代数方法提供了一个统一的框架，它可以捕获结构上不同的模态逻辑的语义，包括分级和概率模态逻辑和联盟逻辑。在本文中，我们介绍了coalgebraic μ演算，一般（coalgebraic）框架的扩展与不动点算子。我们的主要结果是相关的Tableau演算的完整性和EXPTIME的可判定性守护公式。从技术上讲，这是通过将可满足性减少到非良基场景的存在来实现的，而非良基场景的存在又相当于平价博弈中获胜策略的存在。我们的结果是参数的基础类的模型和产量，作为具体的应用，以前未知的复杂性界限的概率μ演算和扩展的联盟逻辑与不动点。

香草式相继式演算即按值调用（新视角）

The Vanilla Sequent Calculus is Call-by-Value (Fresh Perspective)

本文证明最小直觉主义逻辑中最基本的相继式演算（香草式）可自然地解释为按值调用求值，通过建立与已知形式主义的互模拟实现。

微分精化逻辑的一致替换

Uniform Substitution for Differential Refinement Logic

本文提出微分精化逻辑dRL的一致替换演算，扩展微分动态逻辑dRL以同时推理混合系统性质与关系，用一致替换实现精简可靠的证明器微内核，并证明dRL的精化在混合程序片段上可判定。

直觉正规模态逻辑的演算

Calculi for Intuitionistic Normal Modal Logic

本文给出了一个按名称调用和一个按值调用的项演算，它们都与直觉模态逻辑IK的盒片段有Curry-Howard对应关系。显示了结石的强归一化性和汇合性。此外，我们还定义了一个从按值调用演算到按名称调用演算的CPS转换，并证明了它的可靠性和完备性。

循环演算和抽象资源语义学导论

Introduction to Cirquent Calculus and Abstract Resource Semantics

本文介绍了一种改进的微积分的方法，称为cirquent演算。而在Gentzen风格的证明树兄弟姐妹（或堂兄弟姐妹等）序列是不相交的公式序列，在圆微积分中，它们可以共享元素。明确地允许或禁止共享资源，从而将子结构逻辑的资源感知直觉带到一个更微妙的层次，cirquent演算提供了比cirquent演算更大的灵活性和功能。随着可计算性逻辑的诞生，对新的演绎工具的需求也随之而来（见http：//www.cis.upenn.edu/linggiorgi/cl.html）--这是一种语义构建的计算资源形式理论，它顽固地抵制了传统句法方法框架内的任何公理化尝试。循环微积分打破了僵局。从其规则的全部集合中去除收缩，产生了可计算性逻辑的基本片段CL 5的健全和完整的系统。另一方面，在微积分中做同样的事情，会把婴儿和洗澡水一起扔掉，导致严格较弱的仿射逻辑。可计算性逻辑的一个隐含的主张是，它是CL 5，而不是仿射逻辑，充分体现了传统上与后者相关的资源哲学。为了加强这一主张，本文进一步引入了一个抽象的资源语义，并显示了CL 5的可靠性和完整性。

带有单一替换的类型理论

Type Theory with Single Substitutions

本文为类型理论定义了仅含单一替换和弱化的单一替换演算（SSC），证明了其语法与带族范畴（CwF）语法同构，为定义类型理论提供了极简替代方案。

具有交换模态的Lambek演算

On the Lambek Calculus with an Exchange Modality

本文介绍了交换/非交换逻辑（CNC逻辑）和CNC逻辑的两种范畴模型。这项工作抽象本顿的线性/非线性逻辑通过删除交换结构规则的存在。人们应该把这个逻辑看作是由两个逻辑组成的;一个坐在另一个的左边。左边是直觉线性逻辑，右边是Lambek演算的混合交换/非交换形式化。然后这两个逻辑通过一对monoidal伴随函子连接。然后，在逻辑中使用双方之间的附加可导出交换模态。因此，伴随函子允许将交换结构规则从左侧拉到右侧。然后，我们给出了一个单值附加的范畴模型，然后给出了一个辩证兰贝克空间的具体模型。

通信混合程序的动态逻辑的均匀替换

Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs

本文为通信混合程序的动态逻辑提出均匀替换演算，通过公理替代公理模式并集中健全性检查，简化了含通信与并行性的混合系统证明器实现。

A Gödel Calculus for Linear Temporal Logic

We consider Gödel temporal logic ($\sf GTL$), a variant of linear temporal logic based on Gödel--Dummett propositional logic. In recent work, we have shown this logic to enjoy natural semantics both as a fuzzy logic and as a superintuitionistic logic. Using semantical methods, the logic was shown to be {\sc pspace}-complete. In this paper we provide a deductive calculus for $\sf GTL$, and show this calculus to be sound and complete for the above-mentioned semantics.

幂等指数模态线性逻辑的一个注记

Linear logic with idempotent exponential modalities: a note

本文讨论了幂等指数模态线性逻辑的一个变体。我们提出了一个新的演算系统，并讨论了它的语义。我们还给出了这种演算的具体关系模型。

双直觉逻辑的无割序列演算：扩展版本

A Cut-free Sequent Calculus for Bi-Intuitionistic Logic: Extended Version

双直觉主义逻辑是直觉主义逻辑的推广，它具有一个与蕴涵有关的联结对偶。双直觉逻辑是由Rauszer作为具有代数和Kripke语义的Hilbert演算引入的。但她随后对BiInt的"无切“演算最近被Uustalu证明是失败的。我们提出了一个新的切割免费的BiInt演算，并证明它的声音和完整的Kripke语义。确保完整性是复杂的含义和它的对偶之间的相互作用，类似于未来和过去的时态逻辑模态。我们的演算处理这种相互作用，使用扩展序列传递信息的前提下的结论，使用实例化的变量在失败的派生树的叶子。我们简单的终止论证允许我们的演算用于自动演绎，尽管这不是它的主要目的。

轻逻辑与按值调用λ演算

Light Logics and the Call-by-Value Lambda Calculus

所谓的轻逻辑已经被引入作为具有相当显著的规范化性质的逻辑系统。然而，从这些逻辑为纯λ演算设计类型分配系统是有问题的。在本文中，我们表明，从通常的按名称调用的转换到按值调用的λ演算允许恢复与底层逻辑的强连接。这将在基本仿射逻辑（EAL）的上下文中完成，设计一个自然演绎风格的类型系统，将EAL公式分配给lambda项。

带控制的按需调用类型化$$λ$$演算的可实现性解释与规范化

Realizability Interpretation and Normalization of Typed Call-by-Need $$λ$$-calculus With Control

我们定义了一个变体的可实现性，其中实现者是一个长期和一个替代对。这个变体允许我们证明一个简单类型的按需调用$$λ$-$calculus with control due to Ariola et al. Indeed, in such call-by-need calculus, substitutions have to be delayed until knowing if an argument is really needed. In a second step, we extend the proof to a call-by-need $$ λ$-演算的规范化，该演算配备了一个等价于经典二阶谓词逻辑的类型系统，代表了向证明按需调用经典二阶算术的规范化迈出的一步，该算术由第二作者引入，以提供依赖选择公理的证明即程序解释。

一种自然的直觉主义模态逻辑：公理化与双嵌套演算

A Natural Intuitionistic Modal Logic: Axiomatization and Bi-nested Calculus

本文引入了由前向汇合 Kripke 模型刻画的自然直觉主义模态逻辑 FIK，为其提供了完备的 Hilbert 风格公理化和双嵌套演算，该演算兼具判定程序与有限反模型提取功能。