What is the difference between A-normalization and K-normalization in compilers?
As far as my search-foo led me; K-Normal Form is inspired by A-Normal Form, but instrumented for use in Storage Mode Analysis, which is a static program analysis used for inferring memory mangement directives for functional programs.

The term seems to originate from the following publication:
L. Birkedal, M. Tofte, and M. Vejlstrup. From region inference to von Neumann machines via region representation inference.

A copy of the publication can at the time of writing be obtained from L.Birkedal's faculty webpage under publications.