57 Only in the last few years, theorem provers have become good enough |
57 Only in the last few years, theorem provers have become good enough |
58 for establishing the correctness of some standard lexing and |
58 for establishing the correctness of some standard lexing and |
59 parsing algorithms. For this, the algorithms need to be formulated |
59 parsing algorithms. For this, the algorithms need to be formulated |
60 in way so that it is easy to reason about them. In earlier work |
60 in way so that it is easy to reason about them. In earlier work |
61 about lexing and regular languages, the authors showed that this |
61 about lexing and regular languages, the authors showed that this |
62 precludes algorithms working over graphs. However regular |
62 precludes well-known algorithms working over graphs. However regular |
63 languages can be formulated and reasoned about entirely in terms |
63 languages can be formulated and reasoned about entirely in terms |
64 regular expressions, which can be easily represented in theorem |
64 regular expressions, which can be easily represented in theorem |
65 provers. This work uses the device of derivatives of regular |
65 provers. This work uses the device of derivatives of regular |
66 languages. We like to extend this work to parsers and grammars. |
66 expressions. We like to extend this device to parsers and grammars. |
67 The aim is to come up with elegant and useful parsing algorithms |
67 The aim is to come up with elegant and useful parsing algorithms |
68 whose correctness and absence of bugs can be certified in a theorem |
68 whose correctness and the absence of bugs can be certified in a |
69 prover. |
69 theorem prover. |
70 \mbox{}\\[15cm] |
70 \mbox{}\\[15cm] |
71 |
71 |
72 \noindent |
72 \noindent |
73 |
73 |
74 %\small |
74 %\small |