λ-Q# is an idealized version of Q# aimed at providing it a formal language definition, placing the language on a solid mathematical foundation, and enabling further evolution of its design and type system.