Geodesic
KAT and PHL in Coq
Computer Science and Information Systems, Tome 5 (2008) no. 2.

Voir la notice de l'article provenant de la source Computer Science and Information Systems website

In this article we describe an implementation of Kleene algebra with tests (KAT) in the Coq theorem prover. KAT is an equational system that has been successfully applied in program verification and, in particular, it subsumes the propositional Hoare logic (PHL). We also present an PHL encoding in KAT, by deriving its deduction rules as theorems of KAT. Some examples of simple program’s formal correctness are given. This work is part of a study of the feasibility of using KAT in the automatic production of certificates in the context of (source-level) Proof-Carrying-Code (PCC).
Keywords: Kleene algebra with tests, Hoare logics, interactive theorem proving, and formal verification of software 
@article{CSIS_2008_5_2_a9,
     author = {David Pereira and Nelma Moreira},
     title = {KAT and {PHL} in {Coq}},
     journal = {Computer Science and Information Systems},
     publisher = {mathdoc},
     volume = {5},
     number = {2},
     year = {2008},
     url = {http://geodesic.mathdoc.fr/item/CSIS_2008_5_2_a9/}
}
TY  - JOUR
AU  - David Pereira
AU  - Nelma Moreira
TI  - KAT and PHL in Coq
JO  - Computer Science and Information Systems
PY  - 2008
VL  - 5
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/CSIS_2008_5_2_a9/
ID  - CSIS_2008_5_2_a9
ER  - 
%0 Journal Article
%A David Pereira
%A Nelma Moreira
%T KAT and PHL in Coq
%J Computer Science and Information Systems
%D 2008
%V 5
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/CSIS_2008_5_2_a9/
%F CSIS_2008_5_2_a9
David Pereira; Nelma Moreira. KAT and PHL in Coq. Computer Science and Information Systems, Tome 5 (2008) no. 2. http://geodesic.mathdoc.fr/item/CSIS_2008_5_2_a9/