Partial Derivative Automata Formalized in Coq
From MaRDI portal
Publication:3073622
DOI10.1007/978-3-642-18098-9_7zbMATH Open1297.68214OpenAlexW1638179998MaRDI QIDQ3073622FDOQ3073622
David P. Pereira, José Bacelar Almeida, Simão Melo de Sousa, Nelma Moreira
Publication date: 11 February 2011
Published in: Implementation and Application of Automata (Search for Journal in Brave)
Full work available at URL: http://hdl.handle.net/1822/13097
Cites Work
- Title not available (Why is that?)
- Derivatives of Regular Expressions
- Partial derivatives of regular expressions and finite automaton constructions
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- A completeness theorem for Kleene algebras and the algebra of regular events
- Rewriting extended regular expressions
- On the Average Number of States of Partial Derivative Automata
- On the completeness of propositional Hoare logic
- From Mirkin's prebases to Antimirov's word partial derivatives
- Testing the equivalence of regular languages
- ANTIMIROV AND MOSSES'S REWRITE SYSTEM REVISITED
Cited In (10)
- Deciding Regular Expressions (In-)Equivalence in Coq
- A Decision Procedure for Regular Expression Equivalence in Type Theory
- A formalisation of the Myhill-Nerode theorem based on regular expressions
- Prefix and Right-Partial Derivative Automata
- Deciding Kleene algebra terms equivalence in Coq
- Automating Side Conditions in Formalized Partial Functions
- Behavioural differential equations: a coinductive calculus of streams, automata, and power series
- Two-Way Automata in Coq
- Pumping, with or without choice
- The Picard Algorithm for Ordinary Differential Equations in Coq
Uses Software
This page was built for publication: Partial Derivative Automata Formalized in Coq
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3073622)
