Dana N. Xu

Postdoc at INRIA Grenoble -- Rhone-Alpes

New webpage is here.

Education

Ph.D. student, Computer Laboratory, University of Cambridge
M.Sc. (by research), School of Computing, National University of Singapore
B.Comp. (Hons), School of Computing, National University of Singapore

Teaching

Part II

Types (2004, 2005, 2006 and 2008)
Specification & Verification I (2006)

Current Research

Current Research Interest

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.

Thesis submission date: 1st Aug 2008

Viva date: 10th Oct 2008

Dana N. Xu's Ph.D. Thesis (.ps, .pdf)

Publications

Dana N. Xu's publications from the DBLP Bibliography Server
Note: APLAS2000-2002 are non-refereed workshops (by invitation only). APLAS2003 onwards are refereed symposiums.

Talks

Static Contract Checking for Haskell -- The Whole Story (ppt, pdf) presented at
- University of Tokyo / National Institute of Informatics Joint Seminar in Japan in Aug 2008
- Queen Mary / Imperial College Joint Seminar in July 2008
- Oxford University in Apr 2008
- Microsoft Research Redmond in Jan 2008
Static Contract Checking for Haskell (ppt) presented at
- National University of Singapore at the end of Nov. 2007
- University of York (Fun in the Afternoon) in late Nov. 2007
- University of Kent (TCS group) in mid Nov. 2007
- IFL'07@Freiburg, Germany (non-refereed) in Sept. 2007
- CPRG-talk@CL.CAM in June 2007
HW'2006@Portland,Oregon,USA: Extended Static Checking for Haskell (ESC/Haskell) (pdf, ppt)
Jan2005@Heriot-Watt University: Modular Inference for Array Checks Optimization (pdf)
APLAS'2004@Taipei: PType System: A Featherweight Parallelizability Detector (pdf)
ASIA-PEPM'2002@Aizu,Japan: Compiling real time functional reactive programming (ppt)
Aug-Sep2002@University of Tokyo (Visiting Masato Takeichi and Zhenjiang Hu's research group)
1. Introduction to Sized Type Inference (ppt)
2. Deriving Preconditions for Array Bound Check Elimination (ppt)

Past Projects

DSEL : Abstract Interpretation for Domain Specific Embedded Language
Formal Automatic Array Bound Checks Elimination for Imperative Program (abce.ps)
Type Based Approach to Parallelization (MSc project)
- Supervisor: Siau-Cheng Khoo
- Examiners: Abhik Roychoudhury and Seif Haridi
- Thesis Score: No Amendment
Extending sized type with collection analysis
Compiling Real-Time Functional Reactive Programming (RT-FRP) to Automata (Hons year project)
Precondition inference for Array Bound Checks Elimination for functional Program (UROP-II project)
Calculating Sized Types (UROP-I project)

*UROP: Undergraduate Research Opportunity Program

Bibles

Introduction to Functional Programming by Richard Bird
The Implementation of Functional Programming Languages by Simon Peyton Jones
Types and Programming Languages by Benjamin C. Pierce
Principles of Program Analysis by Flemming Nielson, Hanne Riis Nielson, Chris Hankin

Proceedings

[ICFP | POPL | PLDI | PEPM | Haskell]

Hobbies

Cooking => My Dining Table
Travelling + Photographing = My Gallery
Hiking, Cycling, Skiing
Reading
- Favourite travel guide: Lonely Planet
- Chinese newspaper: United Morning News (Lianhe Zaobao) (favourite columnist: Yu Shiyu)
- Chinese Classical Literature (in Archaic Chinese)
- Western Classic Novels (in Modern English)
Watching
- DVDs: Lovefilm DVD Rental by Post
- BBC news : BBC Video News (free)
Dreaming, Thinking

Motto: The foolish man seeks happiness in the distance, the wise grows it under his feet. -- James Oppenheim

(0.13°E,52.21°N)