KAT and PHL in Coq

• Type: Article in International Scientific Journal
• Date: 2008

Authors

David Pereira (Author) Other; Nelma Moreira (Author) FCUP

Journal

Title: Computer Science and Information Systems

Vol. 5

Pages: 137-160

ISSN: 1820-0214

Publisher: ComSIS Consortium

Indexing

ISI Web of Knowledge - 2 Citations

Scopus - 5 Citations

Scientific classification

FOS: Natural sciences > Computer and information sciences

Other information

Authenticus ID: P-003-TD0

DOI: 10.2298/csis0802137p

Abstract (EN): 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).

Language: English

Type (Professor's evaluation): Scientific

No. of pages: 24