Kleene Algebra with Tests and Coq Tools for while Programs

DOI10.1007/978-3-642-39634-2_15zbMath1317.68229arXiv1302.1737OpenAlexW1646862118MaRDI QIDQ5327344

Damien Pous

Publication date: 7 August 2013

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1302.1737

Mathematics Subject Classification ID

Logic in computer science (03B70) Algebraic theory of languages and automata (68Q70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (12)

Using relation-algebraic means and tool support for investigating and computing bipartitions ⋮ Reasoning About Cardinalities of Relations with Applications Supported by Proof Assistants ⋮ Algorithms for Kleene algebra with converse ⋮ Regular language representations in the constructive type theory of Coq ⋮ Unnamed Item ⋮ On tools for completeness of Kleene algebra with hypotheses ⋮ Completeness for Identity-free Kleene Lattices ⋮ Hoare Semigroups ⋮ Unnamed Item ⋮ Building program construction and verification tools from algebraic principles ⋮ Cardinality of relations with applications ⋮ Cardinalities of Finite Relations in Coq

Uses Software

• Coq

This page was built for publication: Kleene Algebra with Tests and Coq Tools for while Programs