Call-by-value Termination in the Untyped lambda-calculus, Journal Logical Methods in Computer Science. HERE.
The Semantics of ``Semantic Patches" in Coccinelle. (paper D-567 in ToppsBib).
Flow Analysis of Lazy Higher Order Functional Programs. (paper D-562 in ToppsBib).
By others at DIKU, and directly related to my research:
Computational Complexity via Programming Languages: Constant Factors Do Matter. Copyright Springer-Verlag, Springer version here
Partial Evaluation and Automatic Program Generation. (book, postscript can be downloaded)
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)
A Self-Applicable Partial Evaluator for the Lambda Calculus. (Postscript not available. See newer version in Chapter 8 of Partial Evaluation book.)