Partial Derivative Automata Formalized in Coq

DOI10.1007/978-3-642-18098-9_7zbMath1297.68214OpenAlexW1638179998MaRDI QIDQ3073622

David P. Pereira, Simão Melo de Sousa, Nelma Moreira, José Bacelar Almeida

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

Mathematics Subject Classification ID

Related Items (4)

Deciding Regular Expressions (In-)Equivalence in Coq ⋮ A Decision Procedure for Regular Expression Equivalence in Type Theory ⋮ Deciding Kleene algebra terms equivalence in Coq ⋮ A formalisation of the Myhill-Nerode theorem based on regular expressions

Uses Software

• Coq

Cites Work

• Partial derivatives of regular expressions and finite automaton constructions
• Rewriting extended regular expressions
• 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
• On the completeness of propositional Hoare logic
• ANTIMIROV AND MOSSES'S REWRITE SYSTEM REVISITED
• On the Average Number of States of Partial Derivative Automata
• Derivatives of Regular Expressions
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Partial Derivative Automata Formalized in Coq