equal
deleted
inserted
replaced
1127 |
1127 |
1128 Closely related to our work is an automata-based lexer formalised by |
1128 Closely related to our work is an automata-based lexer formalised by |
1129 Nipkow \cite{Nipkow98}. This lexer also splits up strings into longest |
1129 Nipkow \cite{Nipkow98}. This lexer also splits up strings into longest |
1130 initial substrings, but Nipkow's algorithm is not completely |
1130 initial substrings, but Nipkow's algorithm is not completely |
1131 computational. The algorithm by Sulzmann and Lu, in contrast, can be |
1131 computational. The algorithm by Sulzmann and Lu, in contrast, can be |
1132 implemented with easy in any functional language. A bespoke lexer for the |
1132 implemented with ease in any functional language. A bespoke lexer for the |
1133 Imp-language is formalised in Coq as part of the Software Foundations book |
1133 Imp-language is formalised in Coq as part of the Software Foundations book |
1134 by Pierce et al\cite{Pierce2015}. The disadvantage of such bespoke lexers is that they |
1134 by Pierce et al \cite{Pierce2015}. The disadvantage of such bespoke lexers is that they |
1135 do not generalise easily to more advanced features. |
1135 do not generalise easily to more advanced features. |
1136 Our formalisation is available from |
1136 Our formalisation is available from |
1137 \url{http://www.inf.kcl.ac.uk/staff/urbanc/lex}.\medskip |
1137 \url{http://www.inf.kcl.ac.uk/staff/urbanc/lex}.\medskip |
1138 |
1138 |
1139 \noindent |
1139 \noindent |