[pt] Linguagens dinamicamente tipadas, tais como Lua, não usam tipos estáticos em favor de simplicidade e exibilidade, porque a ausência de tipos estáticos significa que programadores não precisam se preocupar em abstrair tipos que devem ser validados por um verificador de tipos. Por outro lado, linguagens estaticamente tipadas ajudam na detecção prévia de diversos bugs e também ajudam na estruturação de programas grandes. Tais pontos geralmente são vistos como duas vantagens que levam programadores a migrar de uma linguagem dinamicamente tipada para uma linguagem estaticamente tipada, quando os pequenos scripts deles evoluem para programas complexos. Sistemas de tipos opcionais nos permitem combinar tipagem dinâmica e estática na mesma linguagem, sem afetar a semântica original da linguagem, tornando mais fácil a evolução de código tipado dinamicamente para código tipado estaticamente. Desenvolver um sistema de tipos opcional para uma linguagem dinamicamente tipada é uma tarefa desafiadora, pois ele deve ser o mais natural possível para os programadores que já estão familiarizados com essa linguagem. Neste trabalho nós apresentamos e formalizamos Typed Lua, um sistema de tipos opcional para Lua, o qual introduz novas características para tipar estaticamente alguns idiomas e características de Lua. Embora Lua compartilhe várias características com outras linguagens dinamicamente tipadas, em particular JavaScript, Lua também possui várias características não usuais, as quais não estão presentes nos sistemas de tipos dessas linguagens. Essas características incluem funções com aridade flexível, atribuições múltiplas, funções que são sobrecarregadas no número de valores de retorno e a evolução incremental de registros e objetos. Nós discutimos como Typed Lua tipa estaticamente essas características e também discutimos nossas decisões de projeto. Finalmente, apresentamos uma avaliação de resultados, a qual obtivemos ao usar Typed Lua para tipar código Lua existente. / [en] Dynamically typed languages such as Lua avoid static types in favor of simplicity and exibility, because the absence of static types means that programmers do not need to bother with abstracting types that should be validated by a type checker. In contrast, statically typed languages provide the early detection of many bugs, and a better framework for structuring large programs. These are two advantages of static typing that may lead programmers to migrate from a dynamically typed to a statically typed language, when their simple scripts evolve into complex programs. Optional type systems allow combining dynamic and static typing in the same language, without affecting its original semantics, making easier this code evolution from dynamic to static typing. Designing an optional type system for a dynamically typed language is challenging, as it should feel natural to programmers that are already familiar with this language. In this work we present and formalize the design of Typed Lua, an optional type system for Lua that introduces novel features to statically type check some Lua idioms and features. Even though Lua shares several characteristics with other dynamically typed languages such as JavaScript, Lua also has several unusual features that are not present in the type system of these languages. These features include functions with exible arity, multiple assignment, functions that are overloaded on the number of return values, and the incremental evolution of record and object types. We discuss how Typed Lua handles these features and our design decisions. Finally, we present the evaluation results that we achieved while using Typed Lua to type existing Lua code.