Projects using Turnstile+ and/or the "types-as-macros" approach to creating typed languages.

• Cur: An extensible Coq-inspired proof assistant.

• MLish: A language in the OCaml family with an extensible type system. Implement and use new features like GADTs and type classes as user libraries.

• Typed Video: A typed variant of the Video language that adds Dependent ML-style indexed types.

• Typed Rosette: An typed version of Rosette that guards against lifted symbolic flowing into unlifted contexts.

• CBPV Scheme: A Scheme variant with call-by-push-value semantics.

• Typed Syndicate: An actor-based language supporting a "conversational" model of concurrency.

• Hackett: A language integrating Racket macros and Haskell types.