We present a Natural Deduction proof system for the propositional modal #um#-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 set in presence of recursive constructors,the encoding of modal (sequent-style) rules and of context sensitive grammars.The formalization can be used in the system Coq,providing an experimental computer-aided proof environment for the interactive development of error-free proofs in the #um#-calculus.The techniques we adopt can be readily ported to other languages and proof systems featuring similar problematic issues.
展开▼
