Dear Professor ???

I have recently been appointed as a University Lecturer

at King's College London. I know Chunhan Wu from my earlier 

work with Professor Xingyuan Zhang on regular languages and

the Isabelle theorem prover. This work led to a highly 

regarded publication at an international conference and

we also submitted a journal version of this work. In

both publications, Chunhan did much of the work and

has 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 by

my grant at King's College London. He would work with me

on 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 this

effectively it would be most convenient for us if Chunhan

can 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 know

well researchers in Cambridge and in Munich, where the

theorem prover Isabelle is mainly developed and which

are centres of excellence in the field of automated

reasoning. During these 11 months, Chunhan and I would

work on projects which we hope can be published at

top-tier conferences.

I kindly request that you grant 11 months leave to

Chunhan. I am sure this scientific visit will be

invaluable for his career. He is a bright researcher

who will benefit greatly from collaboration with

established researchers in the field of automated reasoning. 

In due course when all bureaucratic hurdles are taken

the Head of the Informatics Department of King's College 

will also write to you supporting the request to

invite Chunhan to work with me in London.

Yours sincerely, 

Dr Christian Urban

PS: Please find attach an outline of the working plan

between 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.