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
Home page for Neil D. Jones

Neil D. Jones

Professor

Events being organised in 2005

The PAT Summer School on Program analysis and transformation abstract and virtual machines, happens in the week 6.-10 June, 2005.
This one-week summer school, held at the University of Copenhagen, will feature lectures by well-renowned researchers. The common focus of the Summer School is the treatment of programs as data objects, in practice and in theory, and by semantically well-founded methods. Related topics include partial evaluation, program flow analysis, abstract interpretation, optimising compilers, termination analysis, and several sorts of program transformation.
For more information see the PAT Summer School home page.
NWPT'05: the Nordic Workshop on Programming Theory.

Recent and ongoing research work

The Size-Change Principle for Program Termination. (POPL 2001). An automatic and rather general procedure for analyzing termination of first-order programs. Two techniques: one using automata on infinite words, and a more practical one computing the closure of a set of "size-change graphs".
Termination Analysis and Specialization-Point Insertion in Offline Partial Evaluation. (Toplas 2004). This journal paper applies the previous paper's techniques to a harder problem: automatically solving the termination problem for specializers (partial evaluators) and for "generating extensions", the program generators that most offline partial evaluators produce.
Termination analysis of the untyped lambda-calculus. (invited paper for RTA 2004). The size-change principle is extended from first-order programs to the untyped lambda-calulus.

Proving Correctness of Compiler Optimizations by Temporal Logic. (HOSC 2004). Lacey and De Moor showed how classical compiler optimization techniques can be elegantly expressed via rewrite rules conditioned on temporal conditions. This journal paper sets up a framework for proving correctness of such rules, and applies it to three of them (dead code elimination, constant folding, code motion).

Transformation by interpreter specialisation. (SCP 2004). An automatic program transformer may be constructed as the "generating extension" of an interpreter. While a goodly range of transformations may be achieved in this way, the efficiency of the transformed programs depends critically on how the interpreter is written. This journal paper concerns cause and effect in this scenario. It presents both good and bad examples, and enunciates several principles useful to generate efficient transformed programs.

Downloadable papers

List of downloadable papers

Odds and Ends:

Slides from an invited talk held at RTA 2004 (Rewriting Techniques and Applications), with title Termination Analysis of the Untyped Lambda Calculus .
Slides from an invited talk held at PLI (Programs, Logics and Implementations of Higher-order Programming Languages), with title Program Generation, Termination, and Binding-time Analysis .
Book on Computability and Complexity. List of corrections
Partial evaluation book can be downloaded!
Slides from a nontechnical talk held at LIX (Ecole Polytechnique, Paris), with title Programs as Data Objects.
Publications (part of Curriculum vitae)
Curriculum vitae

Coordinates:

Address: DIKU, University of Copenhagen
Universitetsparken 1
DK-2100 Copenhagen East
DENMARK
Phones. Office: 45+ 35321410; central:45+ 35321400; home: 45+ 45868236; fax: 45+ 35321401.

Neil D. Jones ( neil@diku.dk )