1998/09/29 by Marino Miculan, Miculan, Marino
Computer Science · #D.2.4 #F.3.1 #F.4.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Semantic Web and Ontologies #cs.LO
paper · pdf · doi:10.48550/arxiv.cs/9809120
17 pages; longer version of the paper which will appear in Proc. ICTCS'98 (World Scientific)
arxiv created 1998/09/29 · openalex publication_date 1998/09/29 · arxiv updated 2009/11/30 · openalex created_date 2024/04/11 · openalex updated_date 2026/07/28
In this paper, we present a formalization of Kozen's propositional modal μ-calculus, in the Calculus of Inductive 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 (``proof'') rules and of context sensitive grammars. The encoding can be used in the \Coq system, providing an experimental computer-aided proof environment for the interactive development of error-free proofs in the μ-calculus. The techniques we adopted can be readily ported to other languages and proof systems featuring similar problematic issues.