Adding static types to dynamic languages requires balancing expressiveness, safety, and backward compatibility. These trade-offs often limit the practical adoption of type systems. This thesis presents a gradual type system for Elixir grounded in set-theoretic types, where types denote sets of values and support union, intersection, and negation operations.

The central hypothesis is that set-theoretic types are particularly well-suited for capturing the programming patterns of dynamic languages. Union types reflect the branching nature of dynamic programs; intersection types express data flow and function overloading; negation types enable precise analysis of pattern matching by excluding values captured by preceding branches.

A key challenge is articulating gradual typing with semantic subtyping. We represent gradual types as intervals bounded below by the precise static type of all known values and above by the dynamic type of all possible values, enabling fine-grained tracking of type information at the boundaries between typed and untyped code.

On the theoretical side, we present a safe-erasure gradual typing discipline exploiting runtime checks already in the Erlang VM, an extensive typed analysis of pattern matching, and an extension of semantic subtyping to handle Elixir's data structures. To prevent the unchecked spread of dynamic types, we introduce strong function refinements, a crucial aspect for maintaining type safety in a gradually typed system.

On the practical side, we address implementation within the Elixir compiler. We present efficient algorithms and data structures for type operations, evaluate compilation performance, and document design choices that minimize overhead while preserving expressiveness, constituting a guide for language implementers seeking to integrate gradual set-theoretic types into dynamic languages.