Downloadable publications (updated 14 June, 2008)

• 2009:

  Proceedings of VMCAI 2009 (Verification, Model Checking and Abstract Interpretation). (paper D-604 in ToppsBib).

• 2008:

  Call-by-value Termination in the Untyped lambda-calculus, Journal Logical Methods in Computer Science. HERE.

  Interpretive Overhead and Optimal Specialisation. Or: Life without the Pending List (Workshop Version). (META 2008). (paper D-591 in ToppsBib).

  Linear, Polynomial or Exponential? Complexity Inference in Polynomial Time. (paper D-587 in ToppsBib).

  A Flow Calculus of mwp-Bounds for Complexity Analysis. (ACM Transactions on Computational Logic2008). (Paper D-592 in ToppsBib).

• 2007:

  The Semantics of ``Semantic Patches" in Coccinelle. (paper D-567 in ToppsBib).

  Flow Analysis of Lazy Higher Order Functional Programs (for John Reynolds' Festchrift issue of (paper D-562 in ToppsBib).

• 2006:

  Selected Papers of the 17th Nordic Workshop on Programming Theory (NWPT'05). (entry D-549 in ToppsBib).

  By others at DIKU, and directly related to my research:

  Size-change Termination and Bound Analysis.

  On Jones-Optimal Specializers: A Case Study Using Unmix.

• 2005:

  Termination Analysis and Specialization-Point Insertion in Offline Partial Evaluation.

  The Flow of Data and the Complexity of Algorithms.

  Termination Analysis of Higher-Order Functional Programs.

  Redundant Call Elimination via Tupling.

• 2004:

  Compiler optimization correctness by temporal logic.

  Transformation by interpreter specialisation.

  Termination Analysis of the Untyped lambda-Calculus.

• 2002:

  Program Generation, Termination, and Binding-time Analysis.

  Proving Correctness of Compiler Optimizations by Temporal Logic.

• 2001:

  The Size-Change Principle for Program Termination.

  The Expressive Power of Higher-Order Types.

  Marktoberdorf 2001 Lecture Notes: Computability and Complexity from a Programming Perspective.

• 2000:

  Computational Complexity via Programming Languages: Constant Factors Do Matter. Copyright Springer-Verlag, Springer version here

  The Essence of Program Transformation by Partial Evaluation and Driving. dvi.Z

• 1999:

  A precise version of a time hierarchy theorem.

  Partial evaluation of lambda calculus.

  LOGSPACE and PTIME characterized by Programming Languages.

• 1997:

  Higher-Order Minimal Function Graphs , with pointer to electronic journal article.

  Combining Abstract Interpretation and Partial Evaluation (brief overview).

• 1996:

  An Introduction to Partial Evaluation.

  Automatic program specialization by partial evaluation: an introduction.

  BTA Algorithms to Ensure Termination of Off-line Partial Evaluation.

  A Positive Supercompiler.

  What Not to Do When Writing an Interpreter for Specialisation.

• 1995:

  MIX Ten Years Later.

• 1994:

  Abstract Interpretation: a Semantics-Based Tool for Program Analysis.

  Abstract Interpretation and Partial Evaluation in Functional and Logic Programming.

  Program Speedups in Theory and Practice.

  Denotational Abstract Interpretation of Logic Programs.

  Towards Unifying Deforestation, Supercompilation, Partial Evaluation, and Generalized Partial Computation.

• 1993:

  Generalizing Cook's Transformation to Imperative Stack Programs.

  Constant Time Factors Do Matter.

  Partial Evaluation and Automatic Program Generation. (book, postscript can be downloaded)

• 1991:

  Compiler Generation by Partial Evaluation: a Case Study. (Postscript not available. See newer version in Chapter 4 of Partial Evaluation book.)

  A Partial Evaluator for the Untyped Lambda Calculus. (long version, with program code)

  Computer Implementation and Applications of Kleene's S-m-n and Recursion Theorems.

  Efficient Algebraic Operations on Programs.

• 1990:

  A Self-Applicable Partial Evaluator for the Lambda Calculus. (Postscript not available. See newer version in Chapter 8 of Partial Evaluation book.)