Is
a high-performance reflective language and system supporting both
equational and rewriting logic specification and programming for a wide
range of applications.
Is
an analysis tool for cryptographic protocols that takes into account
many of the algebraic properties of crypto systems that are not included
in other tools. These include cancellation of encryption and
decryption, Abelian groups (including exclusive-or), exponentiation, and
homomorphic encryption.
Is
a most advanced formal specification language which inherits many
advanced features (e.g. flexible mix-fix syntax, powerful and clear
typing system with ordered sorts, parameteric modules and views for
instantiating the parameters, and module expressions, etc.) from OBJ algebraic specification language.