Kleene Algebra with Tests and Coq Tools for while Programs
From MaRDI portal
Publication:5327344
DOI10.1007/978-3-642-39634-2_15zbMath1317.68229arXiv1302.1737OpenAlexW1646862118MaRDI QIDQ5327344
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
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
This page was built for publication: Kleene Algebra with Tests and Coq Tools for while Programs
