# HG changeset patch
# User urbanc
# Date 1324563934 0
# Node ID 7823d1b1f14177aab019101b4ed0abf0cb697f59
# Parent  aad64c63960eb924b10f67ebbca50765c8123498
added a draft of the letter for Chunhan

diff -r aad64c63960e -r 7823d1b1f141 CHUNHAN
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CHUNHAN	Thu Dec 22 14:25:34 2011 +0000
@@ -0,0 +1,81 @@
+
+
+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 one 
+year. 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 this one year, Chunhan and I would
+work on projects which we hope can be published at
+top-tier conferences.
+
+I kindly request that you grant a one year 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 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 in London for one year.
+
+
+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. 
+