A Natural Deduction style proof system for propositional $\mu$-calculus and its formalization in inductive type theories

Marino Miculan

In this paper, we present a formalization of Kozen's propositional modal $\mu$-calculus, in the Calculus of Inductive Constructions. We address several problematic issues, such as th…