Visualizing the semantics of gradual languages with Gredex

We present Gredex, an interactive tool to visually explore the static and dynamic semantics of gradually-typed programming languages. Gredex supports a core gradual language with numbers, booleans, functions, pairs, sums, and fixpoints. Gredex displays typing derivations and step-by-step reduction of programs, showing how runtime type information tracking evolves, thereby providing a visual explanation of both successful and failing behaviors. Gredex has been used in multiple research projects over the last decade to design and experiment with gradual languages with features such as security typing, flexible union types, parametric polymorphism, sealing, and merging. Gredex offers a faithful, extensible implementation of gradual language semantics, supporting both experimentation and education.