On Semantic and Type-Theoretic Aspects of Polynomial-Time Computability

This thesis strives to combine two traditions in theoretical computer science: complexity theory and denotational semantics. The recently proposed setting of game semantics, which provided first syntax-independent fully abstract models of many programming languages, is used to characterize the polynomial-time computable functions as those definable by a certain kind of strategies in two-player games. In particular, players must comply with a network protocol that structures the exchange of moves between players and restricts the way games can be modied by them during play. The tight correspondence is achieved through a faithful characterization of the space of proofs in light affine logic, which itself captures polynomial-time computation by the process of cut-elimination. A representation theory of proofs, extending essential nets for intuitionistic linear logic, is developed for light ane logic and serves as a link between proofs and strategies. The nets corresponding to proofs distinguish themselves by satisfying such graph-theoretic properties as acyclicity, domination and well-bracketing. Proofs in normal form are then identified as canonical nets and related to strategies by a full and faithful completeness result. We also investigate the algorithmic content of light affine logic in the form of a simple programming language incorporating a form of safe recursion. The language is demonstrated to express all polynomial-time computable functions and to be compositionally interpretable in the logic which guarantees that it can be executed in polynomial-time using the cut-elimination procedure and also interpreted in the game model. denotational semantics capturing a complexity-theoretic concept. It is hoped that they will initiate an alternative approach to complexity based on the analysis of the semantic content of complexity classes