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 : Static Contract Checking for Haskell
ESC/Haskell works as a backend for the Static Contract Checker (paper, accepted by POPL'09).
The theory behind it can verify sorting algorithms, AVL tree as I have tried those examples out by hand.
I have implemented the contract checker in GHC, trying medium sized programs now.
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 work with Daan Leijen on compiling an experimental functional language (Morrow) to C#. It is a baby step towards compiling Haskell to .Net.