List-coloring embedded graphs without cycles of lengths 4 to 8

The well-known Steinberg's conjecture postulates that every planar graph without 4-cycles and 5-cycles is 3-colorable. The list-coloring version of this claim is known to be false. However, we prove that excluding cycles of lengths 4 to 8 is sufficient to guarantee 3-choosability of a planar graph, thus answering a question of Borodin. For the proof, we use a new variant of graph coloring called correspondence coloring which generalizes list coloring and allows for reductions previously only possible for ordinary coloring.