Deciding Kleene Algebras in Coq
From MaRDI portal
Publication:2881083
DOI10.2168/LMCS-8(1:16)2012zbMath1238.68146MaRDI QIDQ2881083
Publication date: 3 April 2012
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
regular expressionsfinite automatadecision procedureKleene algebra\texttt{Coq} proof assistantreflexive tactictypeclasses
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (12)
Using relation-algebraic means and tool support for investigating and computing bipartitions ⋮ Algorithms for Kleene algebra with converse ⋮ Nominal Kleene Coalgebra ⋮ A Formalisation of Finite Automata Using Hereditarily Finite Sets ⋮ Towards Certifiable Implementation of Graph Transformation via Relation Categories ⋮ Regular language representations in the constructive type theory of Coq ⋮ Deciding Synchronous Kleene Algebra with Derivatives ⋮ Proving language inclusion and equivalence by coinduction ⋮ Unnamed Item ⋮ Refinement to certify abstract interpretations: illustrated on linearization for polyhedra ⋮ Completeness for Identity-free Kleene Lattices ⋮ Two-Way Automata in Coq
Uses Software
This page was built for publication: Deciding Kleene Algebras in Coq
