Weak and strong normalization, K-redexes, and first-order logic. - Peter Møller Neergaard (1999)

Conservation and Uniform Normalization in Lambda Calculi with Erasing Reductions. - Peter Møller Neergaard; Morten Heine Sørensen (Inf. Comput., 2002)

A Functional Language for Logarithmic Space. - Peter Møller Neergaard (APLAS, 2004)

Types, potency, and idempotency: why nonlinearity and amnesia make a type system work. - Peter Møller Neergaard; Harry G. Mairson (ICFP, 2004)

Theoretical Pearls: A bargain for intersection types: a simple strong normalization proof. - Peter Møller Neergaard (J. Funct. Program., 2005)