It is a challenging task to create a well-typed semantic model for a programming language that supports references to dynamically allocated memory cells that may hold values of any type, such as functions or addresses of other cells. The essence of the problem is that of circularity: the type of a reference depends on the store whose content is changed over time, and the type of a store depends on the references contained in it.

The paper addresses this problem by giving the first translation of an imperative language with general references to an extension of System F called FORK, a second-order typed lambda-calculus that is augmented by recursive kinds in order to allow nonterminating computations on the type level; thus, FORK can model recursive types as lambda terms with infinite reductions. The authors show how System F equipped with general references can be translated to FORK and prove that the translation is type preserving; that is, if the untyped reduction of a program with references yields a term of a certain type, the well-typed reduction in FORK also yields that term.

The correctness of the result is substantiated with the help of software: an implementation of the FORK type checker is freely available, as are the language translator and the machine-checked proofs of the soundness theorems. The paper presents an important new result; while being quite technical in nature, it also contains an extensive introduction and explanation of the approach that is accessible to nonexperts in the field.