equal
deleted
inserted
replaced
1238 computational. The algorithm by Sulzmann and Lu, in contrast, can be |
1238 computational. The algorithm by Sulzmann and Lu, in contrast, can be |
1239 implemented with ease in any functional language. A bespoke lexer for the |
1239 implemented with ease in any functional language. A bespoke lexer for the |
1240 Imp-language is formalised in Coq as part of the Software Foundations book |
1240 Imp-language is formalised in Coq as part of the Software Foundations book |
1241 by Pierce et al \cite{Pierce2015}. The disadvantage of such bespoke lexers is that they |
1241 by Pierce et al \cite{Pierce2015}. The disadvantage of such bespoke lexers is that they |
1242 do not generalise easily to more advanced features. |
1242 do not generalise easily to more advanced features. |
1243 Our formalisation is available from |
1243 Our formalisation is available from the Archive of Formal Proofs \cite{aduAFP16} |
1244 \url{http://www.inf.kcl.ac.uk/staff/urbanc/lex}.\medskip |
1244 under \url{http://www.isa-afp.org/entries/Posix-Lexing.shtml}.\medskip |
1245 |
1245 |
1246 \noindent |
1246 \noindent |
1247 {\bf Acknowledgements:} |
1247 {\bf Acknowledgements:} |
1248 We are very grateful to Martin Sulzmann for his comments on our work and |
1248 We are very grateful to Martin Sulzmann for his comments on our work and |
1249 moreover for patiently explaining to us the details in \cite{Sulzmann2014}. We |
1249 moreover for patiently explaining to us the details in \cite{Sulzmann2014}. We |