Executing and Verifying Higher-Order ...
Document type :
Article dans une revue scientifique
Title :
Executing and Verifying Higher-Order Functional-Imperative Programs in Maude
Author(s) :
Journal title :
Journal of Logical and Algebraic Methods in Programming
Pages :
68–91
Publisher :
Elsevier
Publication date :
2017-12
ISSN :
2352-2208
English keyword(s) :
Reachability Logic
state monad
Maude
higher-order function
state monad
Maude
higher-order function
HAL domain(s) :
Informatique [cs]/Logique en informatique [cs.LO]
Informatique [cs]/Langage de programmation [cs.PL]
Informatique [cs]/Langage de programmation [cs.PL]
English abstract : [en]
We incorporate higher-order functions and state monads in Maude, thereby embedding a higher-order functional language with imperative features in the Maude framework. We illustrate, via simple programs in the resulting ...
Show more >We incorporate higher-order functions and state monads in Maude, thereby embedding a higher-order functional language with imperative features in the Maude framework. We illustrate, via simple programs in the resulting language: the concrete and symbolic execution of programs; their verification with respect to properties expressed in Reachability Logic, a language-parametric generalisation of Hoare Logic; and the verification of program-equivalence properties. Our approach is proved sound and is implemented in Full Maude by taking advantage of its reflective features and module system.Show less >
Show more >We incorporate higher-order functions and state monads in Maude, thereby embedding a higher-order functional language with imperative features in the Maude framework. We illustrate, via simple programs in the resulting language: the concrete and symbolic execution of programs; their verification with respect to properties expressed in Reachability Logic, a language-parametric generalisation of Hoare Logic; and the verification of program-equivalence properties. Our approach is proved sound and is implemented in Full Maude by taking advantage of its reflective features and module system.Show less >
Language :
Anglais
Peer reviewed article :
Oui
Audience :
Internationale
Popular science :
Non
Comment :
(to appear)
Collections :
Source :
Files
- https://hal.inria.fr/hal-01586341/document
- Open access
- Access the document
- https://hal.inria.fr/hal-01586341/document
- Open access
- Access the document
- document
- Open access
- Access the document
- wrla-jlamp-R2.pdf
- Open access
- Access the document
- wrla-jlamp-R2.pdf
- Open access
- Access the document