We present a natural deduction proof system for the propositional modal μ-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 sets in the presence of recursive constructors, and the formalization 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 modal μ-calculus. The techniques we adopt can be readily ported to other languages and proof systems featuring similar problematic issues. © 2001 Academic Press.
On the formalization of the modal mu-calculus in the calculus of inductive constructions / MICULAN, Marino. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - STAMPA. - 164:1(2001), pp. 199-231.
Titolo: | On the formalization of the modal mu-calculus in the calculus of inductive constructions |
Autori: | |
Data di pubblicazione: | 2001 |
Rivista: | |
Citazione: | On the formalization of the modal mu-calculus in the calculus of inductive constructions / MICULAN, Marino. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - STAMPA. - 164:1(2001), pp. 199-231. |
Abstract: | We present a natural deduction proof system for the propositional modal μ-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 sets in the presence of recursive constructors, and the formalization 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 modal μ-calculus. The techniques we adopt can be readily ported to other languages and proof systems featuring similar problematic issues. © 2001 Academic Press. |
Handle: | http://hdl.handle.net/11390/717438 |
Appare nelle tipologie: | 1.1 Articolo in rivista |
File in questo prodotto:
File | Descrizione | Tipologia | Licenza | |
---|---|---|---|---|
IC01.pdf | Documento in Post-print | Non pubblico | Accesso ristretto Richiedi una copia |