Skip to content

Research at St Andrews

POSIX lexing with derivatives of regular expressions (proof pearl)

Research output: ResearchConference contribution


Open Access permissions



Fahad Ausaf, Roy Dyckhoff, Christian Urban

School/Research organisations


Brzozowski introduced the notion of derivatives for regular expressions. They can be used for a very simple regular expression matching algorithm. Sulzmann and Lu cleverly extended this algorithm in order to deal with POSIX matching, which is the underlying disambiguation strategy for regular expressions needed in lexers. Sulzmann and Lu have made available on-line what they call a “rigorous proof” of the correctness of their algorithm w.r.t. their specification; regrettably, it appears to us to have unfillable gaps. In the first part of this paper we give our inductive definition of what a POSIX value is and show (i) that such a value is unique (for given regular expression and string being matched) and (ii) that Sulzmann and Lu’s algorithm always generates such a value (provided that the regular expression matches the string). We also prove the correctness of an optimised version of the POSIX matching algorithm. Our definitions and proof are much simpler than those by Sulzmann and Lu and can be easily formalised in Isabelle/HOL. In the second part we analyse the correctness argument by Sulzmann and Lu and explain why the gaps in this argument cannot be filled easily.


Original languageEnglish
Title of host publicationInteractive Theorem Proving
Subtitle of host publication7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings
EditorsJasmine Christian Blanchette, Stephan Merz
Number of pages18
ISBN (Electronic)9783319431444
ISBN (Print)9783319431437
StatePublished - 2016
EventITP 2016: Interactive Theorem Proving - LORIA Building, Inria Nancy - Grand-Est, Nancy, France
Duration: 22 Aug 201627 Aug 2016
Conference number: 7

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


ConferenceITP 2016: Interactive Theorem Proving
Abbreviated titleITP 2016
Internet address

    Research areas

  • POSIX matching, Derivatives of regular expressions, Isabelle/HOL

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Analyticity, balance and non-admissibility of Cut in Stoic Logic

    Bobzien, S. & Dyckhoff, R. 20 Apr 2018 In : Studia Logica. First Online, 23 p.

    Research output: Research - peer-reviewArticle

  2. Intuitionistic decision procedures since Gentzen

    Dyckhoff, R. 5 May 2016 Advances in Proof Theory. Kahle, R., Strahm, T. & Studer, T. (eds.). Birkhäuser Basel, p. 245-267 (Progress in Computer Science and Applied Logic; vol. 28)

    Research output: Research - peer-reviewChapter (peer-reviewed)

  3. Some remarks on proof-theoretic semantics

    Dyckhoff, R. 2016 Advances in Proof-Theoretic Semantics. Piecha, T. & Schroeder-Heister, P. (eds.). Springer, p. 79-93 15 p. (Trends in Logic; vol. 43)

    Research output: Research - peer-reviewChapter (peer-reviewed)

  4. Geometrisation of first-order logic

    Dyckhoff, R. & Negri, S. Jun 2015 In : Bulletin of Symbolic Logic. 21, 2, p. 123–163 41 p.

    Research output: Research - peer-reviewArticle

ID: 245601547