On the formalization of the Modal μ-Calculus in the Calculus of Inductive Constructions

摘要

We present natural deduction proof system for the propositional modal μ-calculus and its formalization in the calculus of inductive constructions. We address several problematic issues, such as the use of higher-order abstract syntax in inductive sets in the presence of recursive constructors, and the formalization of modal (sequent-style) rules and of context sensitive grammars.