On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions

DOI10.1006/inco.2000.2902zbMath1007.03032OpenAlexW1972691992MaRDI QIDQ1854404

Marino Miculan

Publication date: 14 January 2003

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/inco.2000.2902

zbMATH Keywords

context-sensitive grammarsCoqcalculus of inductive constructionscomputer-aided proof environmentnatural deduction proof systempropositional modal \(\mu\)-calculus

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Inductive definability (03D70)

Related Items

A calculus for attribute-based memory updates, Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts, AbU: a calculus for distributed event-driven programming with attribute-based interaction, Theoretical and practical approaches to the denotational semantics for MDESL based on UTP, Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax

Uses Software

• Coq
• ALF

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Using typed lambda calculus to implement formal systems on a machine
• Results on the propositional \(\mu\)-calculus
• Simple consequence relations
• Local model checking in the modal mu-calculus
• Encoding modal logics in logical frameworks
• \(\pi\)-calculus in (Co)inductive-type theory
• A Constructive Presentation for the Modal Connective of Necessity (□)
• A framework for defining logics
• A natural deduction approach to dynamic logic
• Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski