scientific article; zbMATH DE number 1405663

MaRDI QIDQ4938644zbMATH OpenFDO

Authors Marino Miculan

Publication date 25 April 2000

zbMATH Keywords

Calculus of Inductive Constructionscontext sensitive grammarshigher-order abstract syntaxinteractive development of error-free proofsnatural deduction proof systempropositional modal \(\mu\)-calculus

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Temporal logic (03B44) Grammars and rewriting systems (68Q42)

Recommendations

• On the formalization of the modal -calculus in the calculus of inductive constructions
• On the proof theory of the modal mu-calculus
• Effective cut-elimination for a fragment of modal mu-calculus
• scientific article; zbMATH DE number 7297836
• scientific article; zbMATH DE number 4014064

Cited in

(4)

• On the formalization of the modal -calculus in the calculus of inductive constructions
• scientific article; zbMATH DE number 1059317 (Why is no real title available?)
• On global induction mechanisms in aμ-calculus with explicit approximations
• A Formal Correspondence Between OMDoc with Alternative Proofs and the ${\overline{\lambda}\mu\tilde{\mu}}$ -Calculus

Describes a project that uses

Uses Software

• Coq

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4938644)