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
Recent and ongoing research work
Partial evaluation:
Interpretive Overhead and Optimal Specialisation.
Or: Life without the Pending List (Workshop Version).
(META 2008).
A self-interpreter and a program specialiser with the following
characteristics
are developed for a simple imperative language:
1) The self-interpreter runs with program-independent interpretive
overhead;
2) the specialiser achieves optimal specialisation, that is,
it eliminates all interpretation overhead;
3) the specialiser has been run on a variety of small and large
programs, including specialising the
self-interpreter to itself;
4) all specialiser parts except for loop unfolding have been proven
to terminate.
The specialiser uses two-level binding-time annotations in a new way:
source annotations are used to ensure correctness of
specialised programs.
A novelty: the specialiser has no need for a pending
list, and does no call graph analysis of the residual
program.
CTL and program transformation:
The Semantics of ``Semantic Patches" in Coccinelle.
(APLAS 2007).
A rational formalisation of the core of the Coccinelle
system, used for automating and documenting collateral evolutions in
Linux device drivers. A denotational semantics of the transformation language
is developed.
A richer and more efficient version is defined and
implemented by compiling to the
temporal logic CTL-V. The compilation is
proven correct
and a model check algorithm is
outlined.
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).
Termination-related:
Termination Analysis of Higher-Order Functional Programs (APLAS 2005)
Techniques for size-change termination of the pure untyped
lambda-calculus (RTA 2004) are unified and extended significantly,
to yield a termination analyser for higher-order, call-by-value
programs as in ML's purely functional core or similar functional
languages. The analyser has been proven correct, and implemented for
a substantial subset of OCaml.
Linear, Polynomial or Exponential? Complexity Inference in Polynomial Times
(CIE 2008).
A very natural question about a program is what the growth-rate of its
time complexity is, e.g., is it polynomial. This work is the
first one to completely solve the problem for a well-defined core
language including non-deterministic branching and bounded loops, as
well as restricted arithmetics over integers.
The Flow of Data and the Complexity of Algorithms
(CIE 2005).
A proof system is devised that makes it possible to deduce polynomial
runtime bounds for imperative programs. Further, the system is proven
sound and to have a certain completeness property.
A Flow Calculus of mwp-Bounds for Complexity Analysis
(Transactions on Computational Logic 2008).
Program complexity analysis seems naturally to decompose into two
parts: a termination analysis and a data size analysis.
This paper's aims, given a
program,
to find out whether its variables have acceptable
(polynomially bounded) growth rates.