Neil D. Jones
Slides for ESSLLI Evening Lecture (as of 12 August, 2010)
PDF
Recent and ongoing research work
Remark: There may exist dead links to publications in the Topps
Bibliography (the systems people keep moving things around).
Last resort: many of the papers can be straightforwardly found via
ToppsBib.
(LINKS WORKED ON AGAIN: 17 February 2012; more papers will soon be added).
Programming in Biomolecular Computation:
Programming in Biomolecular Computation;
(CS2BIO 2010,
with Lars Hartmann and Jakob Grue Simonsen).
In spite of widespread discussion about connections between biology and computation, one question is notable by the absence of an answer: where are the programs?
A new "blob" model of computation is presented that is programmable,
and at the same time biologically plausible, storedprogram,
and universal. It is Turing complete in that a universal algorithm (i.e., a selfinterpreter)
exists, able to execute any program,
and not asymptotically inefficient.
Paper [5] is a revised and extended journal version. Paper [7] examines this area
in greater depth and with more extensive connections with computational biology. Paper [10]
(accepted and to appear in journal form in 2012) examines the blob model of computation in
relation to other models that have appeared since Alan Turing's 1936 paper.
Terminationrelated:

SizeChange Termination and
Transition Invariants;
(SAS 2010,
with Matthias Heizmann and Andreas Podelski).
There have been rapid advances in methods for automatically proving program
termination in recent years, both in theoretical research and in applications as
practical as finding termination bugs in device drivers. A recent wave of activity
began with the work on sizechange termination
(Jones, BenAmram, Lee et al), and led to work on
transition invariants (Podelski, Rybalchenko et al). The
difference in the setting has as consequence some apparent incomparability of the analysis and verification methods in these two lines of work.
The goal of this paper is formally to
compare and contrast the two approaches' 1. soundness proofs,
2. abstract domains, and 3. base algorithms.

Termination Analysis of HigherOrder Functional Programs (APLAS
2005;
paper
D540
in
ToppsBib).
Techniques for sizechange termination of the pure untyped
lambdacalculus (RTA 2004) are unified and extended significantly,
to yield a termination analyser for higherorder, callbyvalue
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 lambdacalculus
(2004 conference paper:
D507
in
ToppsBib).
2008 journal version (Logical Methods in Computer Science):
here.
The sizechange principle is extended
from firstorder programs to the untyped lambdacalulus.

The SizeChange Principle for Program Termination
(POPL conference paper
D429
in
ToppsBib).
The ``sizechange termination'' principle for a firstorder
functional language with wellfounded 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.
Program transformation:
 Program transformation by distillation.
Two conference papers [4, 3] (PSI 2011, PEPM 2012) concern transformation by distillation. The
first reformulates distillation as bisimulation between labeled transition systems. The second
gives distillation an improved semantic basis, and explains how superlinear speedups can occur.
(Work connected with a 2010 visit to Dublin City University.)
 Program obfuscation by partial evaluation.
Paper [2] introduces a novel application of partial evaluation (PEPM 2012). It is shown
that specialisation of a ``distorted" selfinterpreter can be used to obfuscate programs, i.e., to
transform them into diculttoanalyze versions that are computionally equivalent.
(Work connected with a 2010 visit to the University of
Verona.)
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, accepted by the Bulletin of Symbolic Logic, to appear in 2012.
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 50odd
years pertaining to the spectrum problem.
Partial evaluation:

Interpretive Overhead and Optimal Specialisation.
Or: Life without the Pending List (Workshop Version).
(META 2008).
A selfinterpreter and a program specialiser with the following
characteristics
are developed for a simple imperative language:
1) The selfinterpreter runs with programindependent 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
selfinterpreter to itself.
Running timerelated:

Linear, Polynomial or Exponential? Complexity Inference in Polynomial
Time
(2005:
paper
D587
in
ToppsBib).
A very natural question about a program is what the growthrate of its
time complexity is, e.g., is it polynomial. This work is the
first one to completely solve the problem for a welldefined core
language including nondeterministic branching and bounded loops, as
well as restricted arithmetics over integers.

The Flow of Data and the Complexity of Algorithms
(2005:
paper
D529
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 mwpBounds 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:

Proving Correctness of Compiler Optimizations by Temporal Logic
(2004: journal
paper
D499
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
List of downloadable papers
Odds and Ends:
Coordinates:
 Home address: Bukkeballevej 88
DK2960 Rungsted Kyst
DENMARK
(retired in 2007 from: DIKU, University of Copenhagen,
Universitetsparken 1,
DK2100 Copenhagen East,
DENMARK)
 Phone. Home: 45+ 4586 8236.
Neil D. Jones
( neil@diku.dk )
Last revised: 3 September, 2011.