J. Berstel, J-E. Pin Local languages and the Berry-Sethi algorithm La construction efficace d'un automate fini à partir d'une ex­ pression rationnelle (régulière) est l'une des tâches principales de la construction d'un compilateur et du traitement de docu­ ments ou d'hypertextes. Le but de cet article est de présenter une preuve formelle de l'algorithme de Berry et Sethi qui met en évidence les liens entre cet algorithme et une famille bien con­ nue de langages reconnaissables, les langages locaux. One of the basic tasks in compiler construction, document pro­ cessing, hypertext software and similar projects is the efficient construction of a finite automaton from a given rational (regu­ lar) expression. The aim of the present paper is to give an expo­ sition and a formal proof of the background for the algorithm of Berry and Sethi relating the computation involved to a well-known family of recognizable languages, the local languages.