Polyadic Approximations in Logic and Computation
Damiano Mazza · HAL (Le Centre pour la Communication Scientifique Directe) · 2017
This document presents some aspects of the research the author carried out roughly between 2012 and 2017. For the sake of uniformity, we chose to focus on a single subject, that of polyadic approximations and their applications to quantitative program analysis and computational complexity. Introduced by Girard, the notion of polyadic approximation is at the basis of a rich theory, with many consequences and applications. We develop it in this thesis, according to the following plan. We start by introducing a 2-operadic approach to the syntax of programming languages, and prove a computational version of Girard's approximation theorem, inducing the notion of polyadic approximation used in the rest of the thesis. We then apply this notion to intersection type systems and computational complexity, concluding with a reformulation of the proof of the Cook-Levin theorem (the result stating that the satisfiability problem is NP-complete) purely in terms of programming languages, approximations and type systems.