Abstract The semantics of gradually typed languages is typically given indirectly via an elaboration into a cast calculus. This contrasts with more conventional formulations of programming language semantics, where the semantics of a language is given directly using, for instance, an operational semantics. This paper presents a new approach to give the semantics of gradually typed languages directly. We use a recently proposed variant of small-step operational semantics called type-directed operational semantics (TDOS). In a TDOS, type annotations become operationally relevant and can affect the result of a program. In the context of a gradually typed language, type annotations are used to trigger type-based conversions on values. We illustrate how to employ a TDOS on gradually typed languages using two calculi. The first calculus, called $\lambda B^{g}$ , is inspired by the semantics of the blame calculus, but it has implicit type conversions, enabling it to be used as a gradually typed language. The second calculus, called $\lambda e$ , explores an eager semantics for gradually typed languages using a TDOS. For both calculi, type safety is proved. For the $\lambda B^{g}$ calculus, we also present a variant with blame labels and illustrate how the TDOS can also deal with such an important feature of gradually typed languages. We also show that the semantics of $\lambda B^{g}$ with blame labels is sound and complete with respect to the semantics of the blame calculus, and that both calculi come with a gradual guarantee . All the results have been formalized in the Coq theorem prover.

@article{paperbot2689,
  title = {Type-directed operational semantics for gradual typing},
  author = {WENJIA YE and BRUNO C. D. S. OLIVEIRA},
  journal = {Journal of Functional Programming},
  volume = {34},
  year = {2024},
  doi = {10.1017/s0956796824000078}
}