Larch/Ada

A language used in the Penelope verification system, to provide semantics for Ada's types. It is notationally similar to Anna.