We present a Natural Deduction proof system for the pro- positional modal μ-calculus, and its formalization in the Calculus of In- ductive 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 (sequent-style) rules and of context sensitive grammars. The formalization can be used in the sy- stem Coq, providing an experimental computer-aided proof environment for the interactive development of error-free proofs in the μ-calculus. The techniques we adopt can be readily ported to other languages and proof systems featuring similar problematic issues. © Springer-Verlag Berlin Heidelberg 1999.

Formalizing a lazy substitution proof system for μ-calculus in the Calculus of Inductive Constructions

MICULAN, Marino
1999

Abstract

We present a Natural Deduction proof system for the pro- positional modal μ-calculus, and its formalization in the Calculus of In- ductive 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 (sequent-style) rules and of context sensitive grammars. The formalization can be used in the sy- stem Coq, providing an experimental computer-aided proof environment for the interactive development of error-free proofs in the μ-calculus. The techniques we adopt can be readily ported to other languages and proof systems featuring similar problematic issues. © Springer-Verlag Berlin Heidelberg 1999.
File in questo prodotto:
File Dimensione Formato  
ICALP99.pdf

accesso aperto

Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 170.87 kB
Formato Adobe PDF
170.87 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11390/678312
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact