28 \LARGE\bf Certified Parsing\\[-10mm] |
28 \LARGE\bf Certified Parsing\\[-10mm] |
29 \mbox{} |
29 \mbox{} |
30 \end{tabular} |
30 \end{tabular} |
31 \end{center} |
31 \end{center} |
32 \thispagestyle{empty} |
32 \thispagestyle{empty} |
33 |
33 \mbox{}\\[-5mm] |
34 \section*{Background} |
|
35 |
|
36 \mbox{}\\[-14mm] |
|
37 |
34 |
38 \begin{multicols}{2} |
35 \begin{multicols}{2} |
|
36 \section*{Background} |
39 \noindent |
37 \noindent |
40 Parsing is the act of transforming plain text into some |
38 Parsing is the act of transforming plain text into some |
41 structure that can be analysed by computers for further processing. |
39 structure that can be analysed by computers for further processing. |
42 One might think that parsing has been studied to death and after |
40 One might think that parsing has been studied to death and after |
43 \emph{yacc} and \emph{lex} no new results can be obtained in this area. |
41 \emph{yacc} and \emph{lex} no new results can be obtained in this area. |
44 However recent results and novel approaches make it increasingly clear, |
42 However recent results and novel approaches make it increasingly clear, |
45 that this is not true anymore. |
43 that this is not true anymore. |
46 |
44 |
47 We propose to approach the subject of parsing from a certification point |
45 We propose to approach the subject of parsing from a certification point |
48 of view. Parsers are increasingly part of certified compilers, like CompCert, |
46 of view. Parsers are increasingly part of certified compilers, like \mbox{\emph{CompCert}}, |
49 which are guaranteed to be correct and bug-free. Such certified compilers are |
47 which are guaranteed to be correct and bug-free. Such certified compilers are |
50 important in areas where software just cannot fail. However, so far the |
48 crucial in areas where software just cannot fail. However, so far the |
51 parsers of these compilers have been left out of the certification. |
49 parsers of these compilers have been left out of the certification. |
52 This is because parsing algorithms are often adhoc and their semantics |
50 This is because parsing algorithms are often adhoc and their semantics |
53 is not clearly specified. Unfortunately, this means parsers can harbour |
51 is not clearly specified. Unfortunately, this means parsers can harbour |
54 errors that potentially invalidate the whole certification and correctness |
52 errors that potentially invalidate the whole certification and correctness |
55 of the compiler. In this project, we like to change that. |
53 of the compiler. In this project, we like to change that. |
64 regular expressions, which can be easily represented in theorem |
62 regular expressions, which can be easily represented in theorem |
65 provers. This work uses the device of derivatives of regular |
63 provers. This work uses the device of derivatives of regular |
66 expressions. We like to extend this device to parsers and grammars. |
64 expressions. We like to extend this device to parsers and grammars. |
67 The aim is to come up with elegant and useful parsing algorithms |
65 The aim is to come up with elegant and useful parsing algorithms |
68 whose correctness and the absence of bugs can be certified in a |
66 whose correctness and the absence of bugs can be certified in a |
69 theorem prover. |
67 theorem prover. |
|
68 |
|
69 \section*{Proposed Work} |
70 \mbox{}\\[15cm] |
70 \mbox{}\\[15cm] |
71 |
71 |
72 \noindent |
72 \noindent |
73 |
73 |
74 %\small |
74 %\small |