Unified correspondence as a proof-theoretic tool. Submitted. Title Suppressed Due to Excessive Length 3

This presentation reports on the results of [11], and focuses on the formal con-nections between correspondence phenomena, well known from the area of modal logic, and the theory of display calculi, originated by Belnap [1]. Sahlqvist correspondence theory. Sahlqvist theory [15] is among the most cele-brated and useful results of the classical theory of modal logic, and one of the hallmarks of its success. It provides an algorithmic, syntactic identification of a class of modal formulas whose associated normal modal logics are strongly complete with respect to elementary (i.e. first-order definable) classes of frames. Unified correspondence. In recent years, building on duality-theoretic insights [7], an encompassing perspective has emerged which has made it possible to export the state-of-the-art in Sahlqvist theory from modal logic to a wide range of logics which includes, among others, intuitionistic and distributive lattice-based (normal modal) logics [5], non-normal (regular) modal logics [14], substructural logics [6], hybrid logics [9], and mu-calculus [2,3]. The breadth of this work has stimulated many and varied applications. Some ar