LOGIC: A Coq Library for Logics.

LOGIC is a Coq library for formalizing logic studies, concerning both logics' applications and logics themselves (meta-theories). For applications, users can port derived rules and efficient proof automation tactics from LOGIC to their own program-logic-based verification projects. For meta-theories, users can easily formalize a standard soundness proof or a Henkin-style completeness proof for logics like classical/intuitionistic propositional logic, separation logic and modal logic with LOGIC's help. In this paper, we present how compositional and portable proof engineering is possible in LOGIC.