Using linear logic and proof theory to unify computational logic

International audienceUsing linear logic and proof theory to unify computational logic by Dale Miller, Inria To be presented at TLLA 17: Trends in Linear Logic and Applications 3 September 2017, Oxford, UK The opening sentence of Girard's 1987 paper introducing linear logic contains the words " Linear logic is a logic behind logic ". In this talk, I will explore a slight variation of this phrase: " Linear logic is the logic behind computational logic ". Switching the indefinite article into a definite article is, of course, dangerous since we do not know what future analysis might reveal. I retain this switch here since, for the scope of this talk, I will not be tempted to consider any alternative to the core principles of linear logic. Also, this latter phrase narrows " logic " to just " computational logic ". By this term, I mean, the discipline that has evolved within theoretical computer science for which there are now several conferences (such as LICS and CSL) as well as journals (such as the Transactions on Computational Logic). In particular, I assume that computational logic includes the following topics: • Logic programming (proof search) • Term representatio