Gradually-Typed Programming Language

Designed and implemented a gradually-typed programming language with CESK abstract machine semantics in OCaml.

Modelled a gradual type-checking system based on academic research in Typed Racket and TypeScript.

Built a complete language toolchain featuring an S-expression parser, static type validators, a linker, and a runtime with detailed state tracing and robust error diagnostics.

Supported arithmetic computation, conditionals, loops, and mixed-type programs with both pre-runtime and runtime checks to enforce soundness across typed and untyped code.