KAT and PHL in Coq | Zendy

David Pereira | Zendy; Nelma Moreira | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

KAT and PHL in Coq

Author(s) -

David Pereira,

Nelma Moreira

Publication year - 2008

Publication title -

computer science and information systems

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.244

H-Index - 24

eISSN - 2406-1018

pISSN - 1820-0214

DOI - 10.2298/csis0802137p

Subject(s) - computer science , correctness , programming language , automated theorem proving , context (archaeology) , proof assistant , gas meter prover , propositional calculus , mathematics , geometry , mathematical proof , paleontology , biology

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). .

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research