Regular_Algebras
From MaRDI portal
Regular Algebras
- A Brief Overview of Agda – A Functional Language with Dependent Types
- A completeness theorem for Kleene algebras and the algebra of regular events
- A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)
- Algebraic notions of nontermination: Omega and divergence in idempotent semirings
- Algebras for iteration and infinite computations
- Algebras for program correctness in Isabelle/HOL
- An efficient Coq tactic for deciding Kleene algebras
- Automatic proof and disproof in Isabelle/HOL
- Complete systems of \(\mathcal B\)-rational identities
- Equational axioms for regular sets
- Formalising foundations of mathematics
- Group axioms for iteration
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Isabelle/HOL. A proof assistant for higher-order logic
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Nitpick: a counterexample generator for higher-order logic based on a relational model finder
- On the fine-structure of regular algebra
- Programming and automating mathematics in the Tarski-Kleene hierarchy
- The new Quickcheck for Isabelle. Random, exhaustive and symbolic testing under one roof
- Tutorial to locales and locale interpretation
- Two Complete Axiom Systems for the Algebra of Regular Events
- Une condition impliquant toutes les identités rationnelles
- Une remarque sur les systèmes complets d'identités rationnelles
Cited in
(4)
This page was built for software: Regular_Algebras
