Formalizing a lazy substitution proof system for μ-calculus in the Calculus of Inductive Constructions

We present a Natural Deduction proof system for the pro- positional modal μ-calculus, and its formalization in the Calculus of In- ductive Constructions. We address several problematic issues, such as the use of higher-order abstract syntax in inductive sets in presence of recursive constructors, the encoding of modal (sequent-style) rules and of context sensitive grammars. The formalization can be used in the sy- stem Coq, providing an experimental computer-aided proof environment for the interactive development of error-free proofs in the μ-calculus. The techniques we adopt can be readily ported to other languages and proof systems featuring similar problematic issues. © Springer-Verlag Berlin Heidelberg 1999.