POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)

DOI10.1007/978-3-319-43144-4_5zbMath1478.68118OpenAlexW2481729626MaRDI QIDQ2829247

Christian Urban, Roy Dyckhoff, Fahad Ausaf

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) Algorithms on strings (68W32) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (3)

POSIX lexing with derivatives of regular expressions ⋮ POSIX Lexing ⋮ POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)

Uses Software

• Archive Formal Proofs
• Regular Sets
• Unnamed Item

Cites Work

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

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