Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Dana N. Xu's homepage
Building reliable and efficient softwares through
static analysis, type theory, program verification and optimization
First year's topic : Arity Analysis
Virtually every compiler performs transformations on the program it is
compiling in an attempt to improve efficiency. However, a
transformation known as "lambda floating" has not received much
attention in the past. In this project we illustrate an analysis
on the arity of a function which determines the number of lambdas that can be
floated out. We give detailed measurements of the effect in an
optimising compiler for the higher-order polymorphic functional
language Haskell.
The approach can be found in arity.ps, which is not ready for publication yet
as the proof and the experiments are not done yet.
Second year's topic : ESC/Haskell
Program errors are common in software systems, including those
that are constructed from advanced programming languages, such as Haskell.
For greater software reliability, such errors should be
reported accurately and detected early during program
development. In this project, we look into an extended
static checking tool for Haskell that allows potential errors
to be accurately and quickly reported. (ESC/Haskell.ps, published in HW'06)
Third year's topic : Sound Haskell
This system is more powerful than the ESC/Haskell system (IFL'07 draft proceeding (non-refereed) pdf ).
I have implemented it in GHC, but still in the debugging stage. Hope it can verify large
programs in real life soon.
My supervisors are Alan Mycroft (Computer Laboratory, University of Cambridge) and Simon Peyton Jones (Microsoft Research in Cambridge).
Internship at Microsoft Research Redmond (Jan-Mar, 2008)
I am working with Daan Leijen on compiling a functional language (Morrow) to C#.