Deciding Kleene algebras in \texttt{Coq}
From MaRDI portal
Publication:2881083
Recommendations
Cited in
(22)- Regular language representations in the constructive type theory of Coq
- Refinement to certify abstract interpretations: illustrated on linearization for polyhedra
- Mac Lane's comparison theorem for the Kleisli construction formalized in Coq
- Deciding Kleene algebra terms equivalence in Coq
- Using relation-algebraic means and tool support for investigating and computing bipartitions
- Two-Way Automata in Coq
- Completeness and Decidability Results for CTL in Coq
- Towards certifiable implementation of graph transformation via relation categories
- Deciding synchronous Kleene algebra with derivatives
- Algorithms for Kleene algebra with converse
- Partial derivative automata formalized in Coq
- Nominal Kleene coalgebra
- A formalisation of finite automata using hereditarily finite sets
- Completeness for identity-free Kleene lattices
- Kleene algebra with tests and Coq tools for while programs
- An efficient Coq tactic for deciding Kleene algebras
- Coinduction: automata, formal proof, companions (invited paper)
- An elementary proof of the FMP for Kleene algebra
- Brzozowski's algorithm for automata minimization verified in Coq
- Incremental algorithms for solving regular expression intersection non-emptiness
- Partial reductions for Kleene algebra with linear hypotheses
- Proving language inclusion and equivalence by coinduction
This page was built for publication: Deciding Kleene algebras in \texttt{Coq}
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2881083)
