CINECA IRIS Institutional Research Information System
IRIS è la piattaforma adottata dall’Università degli Studi di Udine per gestire l’archivio aperto dei prodotti della ricerca. L’archivio contiene articoli, contributi in volume, monografie, interventi pubblicati in atti di convegno, Tesi di dottorato e altri materiali.
EnglishWe 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 |
http://hdl.handle.net/11390/717438
Copyright © 2021