POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)

DOI10.1007/978-3-319-43144-4_5MaRDI QIDQ2829247zbMATHOpenAlexFDO

Authors Fahad Ausaf, Roy Dyckhoff, Christian Urban

Publication date 27 October 2016

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/10023/9472

zbMATH Keywords

Isabelle/HOLderivatives of regular expressionsPOSIX matching

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Grammars and rewriting systems (68Q42) Formalization of mathematics in connection with theorem provers (68V20) Algorithms on strings (68W32)

Recommendations

• POSIX lexing with derivatives of regular expressions
• POSIX regular expression parsing with derivatives
• Regular-expression derivatives re-examined
• Formalising Boost POSIX regular expression matching
• Formalising and implementing Boost POSIX regular expression matching
• Derivatives of regular expressions and an application
• Partial derivatives of an extended regular expression
• Manipulation of regular expressions using derivatives: an overview
• Two-sided derivatives for regular expressions and for hairpin expressions
• Two-sided derivatives for regular expressions and for hairpin expressions

Cites work

• A Decision Procedure for Regular Expression Equivalence in Type Theory
• Adapting functional programs to higher order logic
• Automata, Languages and Programming
• Derivatives of Regular Expressions
• POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)
• POSIX regular expression parsing with derivatives
• Proof Pearl: regular expression equivalence and relation algebra

Cited in

(6)

• Formalising Boost POSIX regular expression matching
• Formalising and implementing Boost POSIX regular expression matching
• POSIX Lexing
• POSIX lexing with derivatives of regular expressions
• POSIX regular expression parsing with derivatives
• POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)

Describes a project that uses

Uses Software

• Isabelle/HOL
• Archive Formal Proofs
• Regular Sets

This page was built for publication: POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2829247)