NIST SP-800 108 seems to have a semi-formal definition in chapter 5.0:
A key derivation function iterates a pseudorandom function (ed: PRF) $n$ times and concatenates the outputs until $L$ bits of keying material are generated, where $n = ⎡L/h⎤$.
For each of the iterations of the PRF, the key derivation key $K_I$ is used as the key, and the input data consists of an iteration variable and a string of fixed input data.
But I must admit that this seems more a description of the inner workings of the described KDF's than a formal definition of one, if such a thing exists.
As about any KDF actually works this way it remains to be seen if this isn't enough of a formal description.
The original HKDF paper has this more formal definition:
Definition 5: A key derivation function (KDF) accepts as input four arguments:
- a value $\sigma$ sampled from a source of keying material (Def. 6),
- a length value $l$,
and two additional arguments,
- a salt
value $r$ defined over a set of possible salt values
- and a context variable $c$,
both of which are optional, i.e., can be set to the null string or to a constant. The KDF output is a string of $l$ bits.