|
1 |
|
2 |
|
3 Dear Professor ??? |
|
4 |
|
5 I have recently been appointed as a University Lecturer |
|
6 at King's College London. I know Chunhan Wu from my earlier |
|
7 work with Professor Xingyuan Zhang on regular languages and |
|
8 the Isabelle theorem prover. This work led to a highly |
|
9 regarded publication at an international conference and |
|
10 we also submitted a journal version of this work. In |
|
11 both publications, Chunhan did much of the work and |
|
12 has been the first author of the papers. |
|
13 |
|
14 I like to invite Chunhan to work with me in London for one |
|
15 year. His living expenses for the stay will be covered by |
|
16 my grant at King's College London. He would work with me |
|
17 on improving the reasoning in the Isabelle theorem prover. |
|
18 I can teach him the internals of this theorem prover so |
|
19 that he can independently implement his own work. To do this |
|
20 effectively it would be most convenient for us if Chunhan |
|
21 can be at King's College London. I can also introduce him |
|
22 there to the research community in the field of automated |
|
23 reasoning. I have worked and got to know |
|
24 well researchers in Cambridge and in Munich, where the |
|
25 theorem prover Isabelle is mainly developed and which |
|
26 are centres of excellence in the field of automated |
|
27 reasoning. During this one year, Chunhan and I would |
|
28 work on projects which we hope can be published at |
|
29 top-tier conferences. |
|
30 |
|
31 I kindly request that you grant a one year leave to |
|
32 Chunhan. I am sure this scientific visit will be |
|
33 invaluable for his career. He is a bright researcher |
|
34 who will benefit greatly from collaboration with |
|
35 established researchers in automated reasoning. |
|
36 In due course when all bureaucratic hurdles are taken |
|
37 the Head of the Informatics Department of King's College |
|
38 will also write to you supporting the request to |
|
39 invite Chunhan to work in London for one year. |
|
40 |
|
41 |
|
42 Yours sincerely, |
|
43 Dr Christian Urban |
|
44 |
|
45 |
|
46 PS: Please find attach an outline of the working plan |
|
47 between Chunhan Wu and me. |
|
48 |
|
49 |
|
50 Work Plan |
|
51 ========= |
|
52 |
|
53 - We first want to investigate how the datatype package |
|
54 of the Isabelle theorem prover can be made more expressive |
|
55 and more efficient. Chunhan in his current work already |
|
56 went to the limits of the capabilities of this package. |
|
57 I have some preliminary results how this state of affairs |
|
58 can be improved and I would work with Chunhan to implement |
|
59 these results. This work is on the cutting edge of research |
|
60 in this field and the hope is it will be published in |
|
61 top-tier conferences and journals. |
|
62 |
|
63 - The second project is about making the Isabelle theorem |
|
64 prover more like a programming environment: programmers should |
|
65 be able to write their code inside a theorem prover, verify |
|
66 properties about the code and then compile it to efficient |
|
67 machine code preserving the guaranties obtained by the verification. |
|
68 These systems are desirable because they can make it cost-effective |
|
69 to verify the functional behaviour of software and allow errors to |
|
70 be detected early during program development. However, to |
|
71 complete this project we will have to make changes to the |
|
72 HOL-logic underlying the Isabelle theorem provers. This |
|
73 is a long-term project which will stretch beyond the time |
|
74 Chunhan can stay in London. But the hope is that preliminary |
|
75 results can already be submitted for publication. |
|
76 |
|
77 - Finally, I like to continue with Chunhan on our work |
|
78 about formalising regular expressions and the Myhill-Nerode theorem. |
|
79 There are still a number of question open, for example how this |
|
80 work can be extended to parsing algorithms. |
|
81 |