1315   For an implementation of a simple regular expression matcher,

  1315   For an implementation of a simple regular expression matcher,

  1316   whose correctness has been formally established, we refer the reader to

  1316   whose correctness has been formally established, we refer the reader to

  1317   Owens and Slind \cite{OwensSlind08}.

  1317   Owens and Slind \cite{OwensSlind08}.

  1318 

  1318 

  1319 

  1319 

  1321   direction and 475 for the second, plus around 300 lines of standard material about

  1321   direction and 475 for the second, plus around 300 lines of standard material about

  1322   regular languages. While this might be seen as too large to count as a

  1322   regular languages. While this might be seen as too large to count as a

  1323   concise proof pearl, this should be seen in the context of the work done by

  1323   concise proof pearl, this should be seen in the context of the work done by

  1324   Constable at al \cite{Constable00} who formalised the Myhill-Nerode theorem

  1324   Constable at al \cite{Constable00} who formalised the Myhill-Nerode theorem

  1325   in Nuprl using automata. They write that their four-member team needed

  1325   in Nuprl using automata. They write that their four-member team needed