We present a translation from the call-by-value λ-calculus to monadic normal forms that includes short-cut boolean evaluation.
The translation is higher-order, operates in one pass, duplicates no code, generates no chains of thunks, and is properly
tail recursive. It makes a crucial use of symbolic computation at translation time.
Basic Research in Computer Science (www.brics.dk), funded by the Danish National Research Foundation.