Formalizing a Lazy Substitution Proof System for -Calculus in the Calculus of Inductive
Constructions Marino Miculan · 1999
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.