Polarized logics, geometry of proofs, and semantics of computation

线性逻辑和证明网是由Girard在1987年提出的，它给计算和证明几何带来了新的思维方式。例如，证明的规范化(对应于对函数式程序的评估)可以按照沿着表示证明的网络(图)中的路径行进来建模。这些旅行是由与证明网的边相关的算子的代数定律控制的。这导致了泛函分析方面的证明的动态语义学，产生了新的算法语义和用于归一化的动态不变量。这就是吉拉德的交互几何(GOI)。在这项工作中，我们将研究交互几何的程序以及所谓的线性逻辑的极化片段，试图找到信息流动力学的模型，以及与复杂性理论和量子编程语言理论的联系。

Linear logic and proof nets, introduced by Girard in 1987, gave rise to new ways of thinking about computation and the geometry of proofs. For example normalization of proofs (which corresponds to evaluation of functional programs) can be modelled in terms of travelling along paths in the nets (graphs) representing proofs. These travels are governed by algebraic laws on operators associated to edges of proof nets. This led to  dynamical semantics of proofs in terms of functional analysis, to a new semantics of algorithms and to dynamical invariants for normalization.   This is Girard's Geometry of Interaction (GoI).    In this work, we shall examine the program of Geometry of Interaction as well as so-called Polarized fragments of linear logic, trying to find models for dynamics of information flow and connections with complexity theory and the theory of quantum programming languages.