PhD defence

Fixpoints of Types in Linear Logic from a Curry-Howard-Lambek Perspective

Abstract. This thesis is concerned with the studying of an extension of the propositional linear logic with fixpoints of type from a Curry-Howard-Lambek perspective. Linear logic with fixpoints of types, called MULL, allows us to have inductive and coinductive proofs. We develop a categorical semantics of MULL based on Seely categories and on strong functors acting on them. Then we introduce and study MULLP as an extension of Polarized Linear Logic, with least and greatest fixpoints. Taking advantage of the implicit structural rules of MULLP, we introduce a term syntax for this language, in the spirit of the classical λ-calculus and of system L. We equip this logical system with a deterministic reduction semantics as well as a categorical semantic. We always examine our categorical semantics with concrete cases such as category of sets and relations, category of sets equipped with a notion of totality (non-uniform totality spaces) and relations preserving, and coherence spaces with totality. In the case of MULLP, we prove an adequacy result for MULLP between its operational and denotational semantics, from which we derive a normalization property thanks to the properties of the totality interpretation. We will also study non-wellfounded proofs in linear logic, which one can see as an extension of inductive proofs, from a denotational semantics point of view by making a relation between validity condition for non-wellfounded proofs and totality interpretation. Finally, we will provide a categorical setting for the exponentials that are encoded using fixpoints operator.