(Co)inductive Proof Systems for Compositional ...
Document type :
Compte-rendu et recension critique d'ouvrage
Title :
(Co)inductive Proof Systems for Compositional Proofs in Reachability Logic
Author(s) :
Rusu, Vlad [Auteur correspondant]
Inria Lille - Nord Europe
Nowak, David [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Inria Lille - Nord Europe
Nowak, David [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Journal title :
Journal of Logical and Algebraic Methods in Programming
Publisher :
Elsevier
Publication date :
2020
ISSN :
2352-2208
HAL domain(s) :
Informatique [cs]/Logique en informatique [cs.LO]
English abstract : [en]
Reachability Logic is a formalism that can be used, among others, for expressing partial-correctness properties of transition systems. In this paper we present three proof systems for this formalism, all of which are sound ...
Show more >Reachability Logic is a formalism that can be used, among others, for expressing partial-correctness properties of transition systems. In this paper we present three proof systems for this formalism, all of which are sound and complete and inherit the coin-ductive nature of the logic. The proof systems differ, however, in several aspects. First, they use induction and coinduction in different proportions. The second aspect regards compositionality, broadly meaning their ability to prove simpler formulas on smaller systems and to reuse those formulas as lemmas for proving more complex formulas on larger systems. The third aspect is the difficulty of their soundness proofs. We show that the more induction a proof system uses, and the more specialised is its use of coinduction (with respect to our problem domain), the more compositional the proof system is, but the more difficult is its soundness proof. We present formalisations of these results in the Coq proof assistant. In particular we have developed support for coinductive proofs that is comparable to that provided by Coq for inductive proofs. This may be of interest to a broader class of Coq users.Show less >
Show more >Reachability Logic is a formalism that can be used, among others, for expressing partial-correctness properties of transition systems. In this paper we present three proof systems for this formalism, all of which are sound and complete and inherit the coin-ductive nature of the logic. The proof systems differ, however, in several aspects. First, they use induction and coinduction in different proportions. The second aspect regards compositionality, broadly meaning their ability to prove simpler formulas on smaller systems and to reuse those formulas as lemmas for proving more complex formulas on larger systems. The third aspect is the difficulty of their soundness proofs. We show that the more induction a proof system uses, and the more specialised is its use of coinduction (with respect to our problem domain), the more compositional the proof system is, but the more difficult is its soundness proof. We present formalisations of these results in the Coq proof assistant. In particular we have developed support for coinductive proofs that is comparable to that provided by Coq for inductive proofs. This may be of interest to a broader class of Coq users.Show less >
Language :
Anglais
Popular science :
Non
Collections :
Source :
Files
- https://hal.inria.fr/hal-02978080/document
- Open access
- Access the document
- http://arxiv.org/pdf/1909.01744
- Open access
- Access the document
- https://hal.inria.fr/hal-02978080/document
- Open access
- Access the document
- https://hal.inria.fr/hal-02978080/document
- Open access
- Access the document
- document
- Open access
- Access the document
- jlamp.pdf
- Open access
- Access the document
- 1909.01744
- Open access
- Access the document