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.