Dear Professor ???I have recently been appointed as a University Lecturerat King's College London. I know Chunhan Wu from my earlier work with Professor Xingyuan Zhang on regular languages andthe Isabelle theorem prover. This work led to a highly regarded publication at an international conference andwe also submitted a journal version of this work. Inboth publications, Chunhan did much of the work andhas been the first author of the papers.I like to invite Chunhan to work with me in London for 11 months. His living expenses for the stay will be covered bymy grant at King's College London. He would work with meon improving the reasoning in the Isabelle theorem prover.I can teach him the internals of this theorem prover so that he can independently implement his own work. To do thiseffectively it would be most convenient for us if Chunhancan be at King's College London. I can also introduce him there to the research community in the field of automated reasoning. I have worked and got to knowwell researchers in Cambridge and in Munich, where thetheorem prover Isabelle is mainly developed and whichare centres of excellence in the field of automatedreasoning. During these 11 months, Chunhan and I wouldwork on projects which we hope can be published attop-tier conferences.I kindly request that you grant 11 months leave toChunhan. I am sure this scientific visit will beinvaluable for his career. He is a bright researcherwho will benefit greatly from collaboration withestablished researchers in the field of automated reasoning. In due course when all bureaucratic hurdles are takenthe Head of the Informatics Department of King's College will also write to you supporting the request toinvite Chunhan to work with me in London.Yours sincerely, Dr Christian UrbanPS: Please find attach an outline of the working planbetween Chunhan Wu and me. Work Plan=========- We first want to investigate how the datatype package of the Isabelle theorem prover can be made more expressive and more efficient. Chunhan in his current work already went to the limits of the capabilities of this package. I have some preliminary results how this state of affairs can be improved and I would work with Chunhan to implement these results. This work is on the cutting edge of research in this field and the hope is it will be published in top-tier conferences and journals.- The second project is about making the Isabelle theorem prover more like a programming environment: programmers should be able to write their code inside a theorem prover, verify properties about the code and then compile it to efficient machine code preserving the guaranties obtained by the verification. These systems are desirable because they can make it cost-effective to verify the functional behaviour of software and allow errors to be detected early during program development. However, to complete this project we will have to make changes to the HOL-logic underlying the Isabelle theorem provers. This is a long-term project which will stretch beyond the time Chunhan can stay in London. But the hope is that preliminary results can already be submitted for publication.- Finally, I like to continue with Chunhan on our work about formalising regular expressions and the Myhill-Nerode theorem. There are still a number of question open, for example how this work can be extended to parsing algorithms.