Polarized logics, geometry of proofs, and semantics of computation

吉拉德在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.