Polarized logics, geometry of proofs, and semantics of computation

点击翻译按钮获取中文摘要

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.