English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We present a Coq library about Kleene algebra with tests, including a proofof their completeness over the appropriate notion of languages, a decisionprocedure for their equational theory, and tools for exploiting hypotheses of aparticular shape in such a theory. Kleene algebra with tests make it possibleto represent if-then-else statements and while loops in most imperativeprogramming languages. They were actually introduced by Kozen as an alternativeto propositional Hoare logic. We show how to exploit the corresponding Coqtools in the context of program verification by proving equivalences of whileprograms, correctness of some standard compiler optimisations, Hoare rules forpartial correctness, and a particularly challenging equivalence of flowchartschemes.

Kleene Algebra with Tests and Coq Tools for While Programs