beta A dependently-typed programming language, aiming to support safe mutable state and a cubical interpretation of univalence.