Neil D. Jones

Recent and ongoing research work

The Spectrum problem:

• Fifty Years of the Spectrum Problem: Survey and New Results by A. Durand, N.D. Jones, J.A. Makowsky and M. More. Preprint, submitted to the Bulletin of Symbolic Logic, July 2009.

  In 1952, Heinrich Scholz published a question in the Journal of Symbolic Logic asking for a characterization of spectra, i.e., sets of natural numbers that are the cardinalities of finite models of first order sentences. Gunter Asser asked whether the complement of a spectrum is always a spectrum. These innocent questions turned out to be seminal for the development of finite model theory and descriptive complexity. Scholz' question was first answered in a 1972 paper by Jones and Selman. Asser's question remains open, as it is closely related to the question P = NP ? In this paper we survey developments over the last 50-odd years pertaining to the spectrum problem.

• Termination Analysis of Higher-Order Functional Programs (APLAS 2005; paper D-540 in ToppsBib). 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.

• Termination analysis of the untyped lambda-calculus (2004 conference paper: D-507 in ToppsBib). 2008 journal version (Logical Methods in Computer Science): here. The size-change principle is extended from first-order programs to the untyped lambda-calulus.

• The Size-Change Principle for Program Termination (POPL conference paper D-429 in ToppsBib). The ``size-change termination'' principle for a first-order functional language with well-founded data is: a program terminates on all inputs if every infinite call sequence (following program control flow) would cause an infinite descent in some data values.

• 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.

Running time-related:

• Linear, Polynomial or Exponential? Complexity Inference in Polynomial Time (2005: paper D-587 in ToppsBib). 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 (2005: paper D-529 in ToppsBib). 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.

CTL and program transformation:

• The Semantics of ``Semantic Patches" (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 (2004: journal paper D-499 in ToppsBib). 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).

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 .

• Book on Computability and Complexity. Revised version can be downloaded! (Many bug fixes, some technical improvements.)

• 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:

• Home address: Bukkeballevej 88
  DK-2960 Rungsted Kyst
  DENMARK
  
  (retired in 2007 from: DIKU, University of Copenhagen, Universitetsparken 1, DK-2100 Copenhagen East, DENMARK)

• Phone. Home: 45+ 4586 8236.